X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek2_encodings.mdwn;h=85d4d77b3b8d77f7e68124f6913afa227cb2923d;hp=6adafda04b2cab617a43baac9d0bdb1b36548586;hb=c70ea8653fd391ba094c8a64419f3532af2076ce;hpb=3303e8c15d71c68c58c6eec5d6dc7c03e3d6d7bd diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn index 6adafda0..85d4d77b 100644 --- a/topics/week2_encodings.mdwn +++ b/topics/week2_encodings.mdwn @@ -423,7 +423,7 @@ And indeed this is the Church encoding of the numbers: 3 ≡ \f z. f (f (f z))         ; or \f z. f3 z ... -The encoding for `0` is equivalent to `\f z. z`, which we've also proposed as the encoding for `[]` and for `false`. Don't read too much into this. +The encoding for `0` is what we also proposed as the encoding for `[]` and for `false`. Don't read too much into this. 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.