undid accidental change to church.ss
svn: r14557
This commit is contained in:
parent
ea861e346f
commit
7334a89d6b
|
@ -5,17 +5,18 @@
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (lambda (x) e)
|
(e (lambda (x) e)
|
||||||
(e e)
|
(let (x e) e)
|
||||||
|
(app e e)
|
||||||
(+ e e)
|
(+ e e)
|
||||||
number
|
number
|
||||||
x)
|
x)
|
||||||
(ctxt (ctxt e)
|
(e-ctxt (lambda (x) e-ctxt)
|
||||||
(v ctxt)
|
a-ctxt)
|
||||||
(+ ctxt e)
|
(a-ctxt (let (x a-ctxt) e)
|
||||||
(+ v ctxt)
|
(app a-ctxt e)
|
||||||
|
(app x a-ctxt)
|
||||||
hole)
|
hole)
|
||||||
(v (lambda (x) e)
|
(v (lambda (x) e)
|
||||||
number
|
|
||||||
x)
|
x)
|
||||||
(x variable))
|
(x variable))
|
||||||
|
|
||||||
|
@ -46,4 +47,11 @@
|
||||||
(subst (x_1 e_1 e_3)))]
|
(subst (x_1 e_1 e_3)))]
|
||||||
[(subst (x_1 e_1 number_1)) number_1])
|
[(subst (x_1 e_1 number_1)) number_1])
|
||||||
|
|
||||||
(apply-reduction-relation reductions `(app (lambda (x) x) (lambda (x) x)))
|
(traces reductions
|
||||||
|
'(let (plus (lambda (m)
|
||||||
|
(lambda (n)
|
||||||
|
(lambda (s)
|
||||||
|
(lambda (z)
|
||||||
|
(app (app m s) (app (app n s) z)))))))
|
||||||
|
(let (two (lambda (s) (lambda (z) (app s (app s z)))))
|
||||||
|
(app (app plus two) two))))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user