From e318627ddbc2c8ae33ee8f3f144c6366e3a14539 Mon Sep 17 00:00:00 2001 From: Harold Carr Date: Mon, 3 Jul 2017 21:17:18 -0700 Subject: [PATCH 1/2] supply missing `in` metafunction --- redex-doc/redex/scribblings/long-tut/mon-aft.scrbl | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl index 45e0f2b5..06b7dee4 100644 --- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl +++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl @@ -207,7 +207,10 @@ Here are two more metafunctions that use patterns in interesting ways: (where #false (in x (x_1 ...)))] [(subtract1 (x ...) x_1) (x ...)]) - +(define-metafunction Lambda + in : x (x ...) -> boolean + [(in x (x_1 ... x x_2 ...)) #true] + [(in x (x_1 ...)) #false]) )) @;% From 730e371d9af6002dd5843b5a28e8d8cd4a40b132 Mon Sep 17 00:00:00 2001 From: Harold Carr Date: Mon, 3 Jul 2017 22:24:14 -0700 Subject: [PATCH 2/2] removed unnecessary Lambda/n - fix test to conform to SD --- redex-doc/redex/scribblings/long-tut/mon-aft.scrbl | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl index 06b7dee4..819244cc 100644 --- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl +++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl @@ -322,15 +322,9 @@ Now α equivalence is straightforward: (racketblock ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent -(define-extended-language Lambda/n Lambda - (e ::= .... n) - (n ::= natural)) - -(define in-Lambda/n? (redex-match? Lambda/n e)) - (module+ test (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true) - (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true) + (test-equal (term (=α (lambda (x) (x x)) (lambda (y) (y y)))) #true) (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false)) (define-metafunction SD