Signed-off-by: Jim Pryor <profjim@jimpryor.net>
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.)
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