From: Chris Barker Date: Sun, 3 Oct 2010 01:07:09 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6dffa91feff41dc4736d907bf59c3a76a3c8d50f;ds=sidebyside edits --- diff --git a/week4.mdwn b/week4.mdwn index ca6eb4ca..b7ff8790 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -289,7 +289,7 @@ lambda calculus. The reason is that each different numberal has a different type! For instance, if zero has type σ, then `false` has type τ --> τ --> &tau, for some τ. Since one is represented by the function `\x.x false 0`, one must have type (τ ---> τ --> &tau) --> &sigma --> σ. But this is a different +--> τ --> τ) --> σ --> σ. But this is a different type than zero! Because each number has a different type, it becomes impossible to write arithmetic operations that can combine zero with one. We would need as many different addition operations as we had