From 21d0ff6296bd67c8828a6968b9e909078aa3aa67 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 14:22:48 -0400 Subject: [PATCH 1/1] week4 tweaking Signed-off-by: Jim Pryor --- week4.mdwn | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/week4.mdwn b/week4.mdwn index 5238b261..78e2d37e 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -69,9 +69,9 @@ succ X ≡ (\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)))) +≡ (\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)) So `succ X` looks like a numeral: it takes two arguments, `s` and `z`, -- 2.11.0