Is there any way to compose contexts in Redex? I want to represent a context where, at each level, the leftmost term is an arbitrary number of nested lambdas, and the hole is in the body of the innermost lambda.
A ::= hole | (\x_1...\x_n.A) e_1 .. e_n Below is my (stripped down) attempt at representing this in redex, but trying to match (term hole) to an A context goes into an infinite loop. #lang racket (require redex) (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (F hole (λ x F)) (L hole (L e)) (A hole (in-hole L (in-hole F A)))) _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
