From 6dffa91feff41dc4736d907bf59c3a76a3c8d50f Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sat, 2 Oct 2010 21:07:09 -0400 Subject: [PATCH] edits --- week4.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.11.0