week4 tweaks

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index e1dcc4e..11eea4c 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -8,7 +8,8 @@ TX` (that's what it means to *have* a fixed point).
 
 <pre><code>let L = \x. T (x x) in
 let X = L L in
-X &equiv; L L &equiv; (\x. T (x x)) L ~~> T (L L) &equiv; T X</code></pre>
+X &equiv; L L &equiv; (\x. T (x x)) L ~~> T (L L) &equiv; T X
+</code></pre>
 
 Please slow down and make sure that you understand what justified each
 of the equalities in the last line.
@@ -27,10 +28,10 @@ A: Right:
 
 <pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
 Y Y &equiv; \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))...)))</code></pre>
+~~> (\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))...)))</code></pre>
 
 #Q: Ouch!  Stop hurting my brain.#
 
@@ -49,9 +50,9 @@ successor.  Let's just check that `X = succ X`:
 <pre><code>let succ = \n s z. s (n s z) in
 let X = (\x. succ (x x)) (\x. succ (x x)) in
 succ X 
-  &equiv; succ ( (\x. succ (x x)) (\x. succ (x x)) ) 
-  ~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
-  &equiv; succ (succ X)</code></pre>
+&equiv; succ ( (\x. succ (x x)) (\x. succ (x x)) ) 
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+&equiv; succ (succ X)</code></pre>
 
 You should see the close similarity with `Y Y` here.