From 335ce8bda8cc7d2bd46710cf024454cca9a21fee Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 3 Oct 2010 13:30:20 -0400 Subject: [PATCH] week4 tweaks Signed-off-by: Jim Pryor --- week4.mdwn | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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. -- 2.11.0