@robby (or other people more expert in redex than I) what’s the best way to generate a fresh variable in a judgment-form while preserving the ability to use the judgement in #:satisfies? Using variable-not-in requires an unquote which #:satisfies complains about.

There isn’t a good way

Mostly because that kind of property will probably make it hard for the generator to be effective

Do you have a suggestion for a redex-friendlier way of doing things? We basically have a unpack form for existential types. Is there a way to check that a variable is fresh, if we specify the variable?

I have some test cases defined on a test submodule:

#lang racket
;; ...
(module+ test
  (provide (all-defined-out))
  (define test-case-1 ___))

How can I interact with these test cases in the Interactions window in DrRacket? I think I should require the test submodule, but I couldn’t find the appropriate require form…

(require (submod "nameofmodule.rkt" test))

Thank you!

All, I was surprised but not necessarily shocked to test a suspicion I had and verify it was true. This is the fact that immutable structs and not necessarily immutable in the sense of being constants. For example: #lang racket (struct vs (h) #:transparent) (define v (vs (make-hash))) (printf "~a~n" v) (hash-set! (vs-h v) 1 1) (printf "~a~n" v) So vs is immutable but that’s because you cannot change what’s in the fields but that doesn’t mean you cannot change the structure as a value. I also haven’t seen this detail being mentioned anywhere - I would have expected something like this to be mentioned in the guide. Maybe I am the only one who finds this counterintuitive for lack of a better word. What do others think?

I would find the opposite suprising — if using an explicitly mutable hash as a field in a struct suddenly made the hash immutable