fixed typo in docs of fresh form
svn: r14556
This commit is contained in:
parent
3b39cfc4b8
commit
ea861e346f
|
@ -5,18 +5,17 @@
|
||||||
|
|
||||||
(define-language lang
|
(define-language lang
|
||||||
(e (lambda (x) e)
|
(e (lambda (x) e)
|
||||||
(let (x e) e)
|
(e e)
|
||||||
(app e e)
|
|
||||||
(+ e e)
|
(+ e e)
|
||||||
number
|
number
|
||||||
x)
|
x)
|
||||||
(e-ctxt (lambda (x) e-ctxt)
|
(ctxt (ctxt e)
|
||||||
a-ctxt)
|
(v ctxt)
|
||||||
(a-ctxt (let (x a-ctxt) e)
|
(+ ctxt e)
|
||||||
(app a-ctxt e)
|
(+ v ctxt)
|
||||||
(app x a-ctxt)
|
|
||||||
hole)
|
hole)
|
||||||
(v (lambda (x) e)
|
(v (lambda (x) e)
|
||||||
|
number
|
||||||
x)
|
x)
|
||||||
(x variable))
|
(x variable))
|
||||||
|
|
||||||
|
@ -47,11 +46,4 @@
|
||||||
(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])
|
||||||
|
|
||||||
(traces reductions
|
(apply-reduction-relation reductions `(app (lambda (x) x) (lambda (x) x)))
|
||||||
'(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))))
|
|
||||||
|
|
|
@ -857,7 +857,7 @@ terminate (it does terminate if the only infinite reduction paths are cyclic).
|
||||||
error elsewhere. }
|
error elsewhere. }
|
||||||
|
|
||||||
@defidform[fresh]{ Recognized specially within
|
@defidform[fresh]{ Recognized specially within
|
||||||
@scheme[reduction-relation]. A @scheme[-->] form is an
|
@scheme[reduction-relation]. A @scheme[fresh] form is an
|
||||||
error elsewhere. }
|
error elsewhere. }
|
||||||
|
|
||||||
@defidform[with]{ Recognized specially within
|
@defidform[with]{ Recognized specially within
|
||||||
|
|
Loading…
Reference in New Issue
Block a user