continuing assignment4

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

diff --git a/assignment4.mdwn b/assignment4.mdwn
index 9f56675..54a3bf2 100644 (file)
--- a/assignment4.mdwn
+++ b/assignment4.mdwn
@@ -81,7 +81,7 @@ Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
 If we gave you such a `Y1` and `Y2`, how would you implement the above definitions of `even` and `odd`?
 
                                        
-<LI>(More challenging.) Using our derivation of Y from the [[Week2]] notes as a model, construct a pair `Y1` and `Y2` that behave in the way described.
+<LI>(More challenging.) Using our derivation of Y from the [Week3 notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave in the way described.
 
 (See [[hints/Assignment 4 hint 4]] if you need some hints.)
 

diff --git a/hints/assignment_4_answer_4.mdwn b/hints/assignment_4_answer_4.mdwn
index 17c8490..c2cd1fd 100644 (file)
--- a/hints/assignment_4_answer_4.mdwn
+++ b/hints/assignment_4_answer_4.mdwn
@@ -13,15 +13,17 @@
                        in
 
 
-       Y1 t1 t2 ~~> elem1 elem1 elem2
+       X1 === Y1 t1 t2 ~~> elem1 elem1 elem2
                         === (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
                         ~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
                        <~~> t1 (Y1 t1 t2) (Y2 t1 t2)
+                        === t1 X1 X2
 
                        and
 
-       Y2 t1 t2 ~~> elem2 elem1 elem2
+       X2 === Y2 t1 t2 ~~> elem2 elem1 elem2
                         === (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
                         ~~> t2 (elem1 elem1 elem2) (elem2 elem1 elem2)
                        <~~> t2 (Y1 t1 t2) (Y2 t1 t2)
+                        === t2 X1 X2