[racket-dev] composing contexts in Redex?

From: Stephen Chang (stchang at ccs.neu.edu)
Date: Mon May 2 15:29:30 EDT 2011

> 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)))))



Posted on the dev mailing list.