I'm wondering, are there any good examples out there of using #:inv with Redex-judgments? Particularly with asserting that some other judgment holds on the output.
For example, I've got: #:contract (SomeJudgment Gamma tt gv gU) #:inv ,(judgment-holds (SomeOtherJudgment gv gU)) The problem I'm having right now is that, if I unquote gv and gU in the invariant, it says they're unbound variables. But if I quote them, it uses the literal terms (term gv) and (term gU), that is, it's not properly binding/substituting gv and gU when it's evaluating the contract. If I add a (begin (println (term gv) ... ) to the contract, it prints 'gv, confirming that the substitution isn't happening. Am I using this wrong? Are there examples of its proper usage, or is this just a mostly-unused feature in Redex? Thanks for all the Redex help! -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
