X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_encodings.mdwn;h=6df8291639c867e0691096fc3dfcfa69ee00da95;hp=c345ac04fc641fd2cab9ac4d63a06ad061031536;hb=4ab26de71d9694f5a65a80cd87d11734cc6aa02b;hpb=9e8d33e04c84ac7e89c32b19a6bff655a546d74c

diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn
index c345ac04..6df82916 100644
--- a/topics/week2_encodings.mdwn
+++ b/topics/week2_encodings.mdwn
@@ -405,4 +405,21 @@ The encoding for `0` can also be written as `\f z. z`, which we've also proposed
 
 Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework.
 
+We saw that using the `cons` operation (Kapulet's `&`) and `[]` as arguments to `fold_right` over a list give us back that very same list. In the Lambda Calculus, that comes to the following:
+
+    [a, b, c] cons []
+
+with the appropriate lambda terms substituted throughout, just reduces to the same lambda term we used to encode `[a, b, c]`.
+
+In the same spirit, what do you expect this will reduce to:
+
+    3 succ 0
+
+Since 3 is `\f z. f (f (f z))`, it should reduce to whatever:
+
+    succ (succ (succ 0))
+
+does. And if we define `succ` properly, we should expect that to give us the same lambda term that we used to encode `3` in the first place.
+
+
 We'll look at other encodings of lists and numbers later.