X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=83d54df1dd9e183364f39143c78d040a9d419ccb;hp=e1dcc4e9a7bd2a15ccc7dea75090061ec9181626;hb=335ce8bda8cc7d2bd46710cf024454cca9a21fee;hpb=3ed508aa627b89b62239723c3f20a971d8f5aed1;ds=inline diff --git a/week4.mdwn b/week4.mdwn index e1dcc4e9..83d54df1 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -27,10 +27,10 @@ A: Right:
let Y = \T. (\x. T (x x)) (\x. T (x x)) in
Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
- ~~> (\x. Y (x x)) (\x. Y (x x))
- ~~> Y ((\x. Y (x x)) (\x. Y (x x)))
- ~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
- ~~> Y (Y (Y (...(Y (Y Y))...)))
+~~> (\x. Y (x x)) (\x. Y (x x))
+~~> Y ((\x. Y (x x)) (\x. Y (x x)))
+~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
+~~> Y (Y (Y (...(Y (Y Y))...)))
#Q: Ouch! Stop hurting my brain.#
@@ -49,9 +49,9 @@ successor. Let's just check that `X = succ X`:
let succ = \n s z. s (n s z) in
let X = (\x. succ (x x)) (\x. succ (x x)) in
succ X
- ≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
- ~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
- ≡ succ (succ X)
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+≡ succ (succ X)
You should see the close similarity with `Y Y` here.