X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week3.mdwn;h=d9c536112218408d951f817641c7d8a5d45ac08f;hp=5d05c700b44cd86f8c6d3b541ee2dc58ab78cfad;hb=70fdac4d0a4db28dc391e3ea13b9c590b6ef9760;hpb=20da31063b4f8c95e219e7364512054e72b6db44
diff --git a/week3.mdwn b/week3.mdwn
index 5d05c700..d9c53611 100644
--- a/week3.mdwn
+++ b/week3.mdwn
@@ -340,9 +340,7 @@ Two of the simplest:
Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))
-Θ′ has the advantage that f (Θ′ f) really *reduces to* Θ′ f.
-
-f (Y′ f) is only convertible with Y′ f; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
+Θ′ has the advantage that f (Θ′ f) really *reduces to* Θ′ f. Whereas f (Y′ f) is only *convertible with* Y′ f; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside Θ′ to just `u u f`? And similarly for Y′?