[racket-dev] composing contexts in Redex?

2011/5/2 Stephen Chang <stchang at ccs.neu.edu>:
>> 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)))))
>

Why not just:

A ::= hole | ((lambda x A) e)

?

Robby