From: Jim Pryor <profjim@jimpryor.net>
Date: Sun, 3 Oct 2010 18:22:48 +0000 (-0400)
Subject: week4 tweaking
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=21d0ff6296bd67c8828a6968b9e909078aa3aa67

week4 tweaking

Signed-off-by: Jim Pryor <profjim@jimpryor.net>
---

diff --git a/week4.mdwn b/week4.mdwn
index 5238b261..78e2d37e 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -69,9 +69,9 @@ succ X
 &equiv; (\n s z. s (n s z)) X 
 ~~> \s z. s (X s z)
 <~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+&equiv; (\n s z. s (n s z)) (\s z. s (X s z))
+~~> \s z. s ((\s z. s (X s z)) s z)
+~~> \s z. s (s (X s z))
 </code></pre>
 
 So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,