diff --git a/collects/redex/examples/delim-cont/meta.rkt b/collects/redex/examples/delim-cont/meta.rkt index fb817fac76..569c2ef592 100644 --- a/collects/redex/examples/delim-cont/meta.rkt +++ b/collects/redex/examples/delim-cont/meta.rkt @@ -14,7 +14,7 @@ [(subst x_1 x_2 (λ (x_3 ...) e_1)) ; shortcut; x_1 != any x_3 (λ (x_3 ...) (subst x_1 x_2 e_1))] [(subst x_1 e_1 (λ (x_2 ...) e_2)) ; x_1 != any x_2 - ,(term-let ([(x_new ...) (variables-not-in (term e_1) (term (x_2 ...)))]) + ,(term-let ([(x_new ...) (variables-not-in (term (x_1 e_1 e_2)) (term (x_2 ...)))]) (term (λ (x_new ...) (subst x_1 e_1 (subst* (x_2 ...) (x_new ...) e_2)))))] [(subst x_1 e_1 x_1) e_1] diff --git a/collects/redex/examples/delim-cont/test.rkt b/collects/redex/examples/delim-cont/test.rkt index d90bdcb2b2..6463f314a1 100644 --- a/collects/redex/examples/delim-cont/test.rkt +++ b/collects/redex/examples/delim-cont/test.rkt @@ -35,6 +35,21 @@ ;; Basic ---------------------------------------- (define (basic-tests) + (test "(λx.e)[y←v] ≠ λy.(e[x←y][y←v])" + '(<> + ([k 4]) [] + (((λ (k1) (λ (k) k)) + (λ () k)) + 0)) + '(<> ([k 4]) [] 0)) + (test "(λx.e)[y←v] ≠ λz.(e[x←z][y←v]) if z ∈ FV(e)" + '(<> + ([k2 5]) + () + (((λ (k1) (λ (k) k2)) + (λ () k)) + 0)) + '(<> ([k2 5]) [] 5)) (test "basic dw" '(<> () [] @@ -995,7 +1010,7 @@ (λ (x) x))))) hole)) 100) - (λ (x) x))))) + (λ (x1) x1))))) (test "similar way to get stuck, but using the pre thunk" '(<> ([output (list)] @@ -1059,7 +1074,7 @@ hole)) 100) 0) - (λ (x) x))))) + (λ (x1) x1))))) (test "loop" '(<> ([counter (list 4 3 2 1 0)])