From: Jim Pryor <profjim@jimpryor.net>
Date: Mon, 4 Oct 2010 00:38:39 +0000 (-0400)
Subject: continuing assignment4
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=075d7652f07175e96cc07ab2392186c4f3524c08

continuing assignment4

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

diff --git a/assignment4.mdwn b/assignment4.mdwn
index 9f566758..54a3bf20 100644
--- 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 17c8490f..c2cd1fd7 100644
--- 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