Fix bad diff
This commit is contained in:
parent
3a98152f33
commit
229e0c8097
|
@ -8,7 +8,7 @@
|
|||
12a11,12
|
||||
> (define the-error "swaps to/from expressions when recurring in the rhs of app")
|
||||
>
|
||||
112a113,114
|
||||
113a114,115
|
||||
> [(subst (M N) x M_x)
|
||||
> ((subst M_x x M) (subst N x M_x))]
|
||||
116,117d117
|
||||
|
|
|
@ -110,9 +110,9 @@
|
|||
[(subst (λ (x_1 τ) M) x_2 v)
|
||||
(λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
|
||||
(where x_new ,(variable-not-in (term (x_1 e x_2))
|
||||
(term x_1)))]
|
||||
[(subst (M N) x M_x)
|
||||
((subst M_x x M) (subst N x M_x))]
|
||||
(term x_1)))]
|
||||
[(subst (c M) x M_x)
|
||||
(c (subst M x M_x))]
|
||||
[(subst M x M_x)
|
||||
|
|
Loading…
Reference in New Issue
Block a user