X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=8d89a5a67a8edac56c403a4b62ee4e7a3f5416eb;hp=10ab8b99c12977afda62d3573a2b6a950dd26d61;hb=c0b23798213c6cb62de42853fea9b5b066588528;hpb=76452415c955f62828e6c81370c9e39eb6d5b28f;ds=sidebyside

diff --git a/week4.mdwn b/week4.mdwn
index 10ab8b99..8d89a5a6 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -1,5 +1,7 @@
 [[!toc]]
 
+#These notes return to the topic of fixed point combiantors for one more return to the topic of fixed point combinators#
+
 Q: How do you know that every term in the untyped lambda calculus has
 a fixed point?
 
@@ -7,9 +9,14 @@ A: That's easy: let `T` be an arbitrary term in the lambda calculus.  If
 `T` has a fixed point, then there exists some `X` such that `X <~~>
 TX` (that's what it means to *have* a fixed point).
 
-   let W = \x.T(xx) in
-   let X = WW in
-   X = WW = (\x.T(xx))W = T(WW) = TX
+<pre>
+let W = \x.T(xx) in
+let X = WW in
+X = WW = (\x.T(xx))W = T(WW) = TX
+</pre>
+
+Please slow down and make sure that you understand what justified each
+of the equalities in the last line.
 
 Q: How do you know that for any term T, YT is a fixed point of T?