[racket-dev] composing contexts in Redex?
> Oh, but this simpler definition seems to be equivalent:
>
> (define-language test
> (e x (λ x e) (e e))
> (x variable-not-otherwise-mentioned)
> (A hole
> (λ x A)
> (A e)))
Yes, you are right. But I left out a part of my grammar, which is that
I need the number of nested lambdas and the number of arguments to be
equal. I couldnt figure out a way to define that with only one
context.
Here's what I'm currently working with:
(F (λ x hole) (λ x F))
(L (hole e) (L e))
(A hole
(side-condition
(in-hole L_1 (in-hole F_1 A))
(= (term (num-λs F_1))
(term (num-args L_1)))))