Redex, when asked to create the compatible closure, creates a context and then uses that. In this case, it will create a context something like this:
TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT) VT ::= (thunk TT) If you want something else (I'm not sure of an algorithm to handle this kind of thing without coming with something like that), it might be simplest to write out the contexts that you want directly and use context-closure. Robby On Fri, May 3, 2019 at 6:42 PM William J. Bowman <w...@williamjbowman.com> wrote: > > Hello all, > > I'm trying to define a model in Redex where values and terms are separate > nonterminals, and then define a reduction relation using `compatible-closure` > to lift the small steps to the, well, compatible closure. > Unfortunately, it doesn't do what I expect, presumably because the > nonterminals > for values and terms are mutually defined, but `compatible-closure` takes > exactly one nonterminal. > > Is there a way to do what I want? > See attached. > > -- > William J. Bowman > > -- > 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. -- 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.
