From b496658969b421a22742f4d77317fef2f8928d7d Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sat, 2 Oct 2010 21:06:52 -0400 Subject: [PATCH] edits --- week4.mdwn | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/week4.mdwn b/week4.mdwn index 9175c4ae..ca6eb4ca 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -288,8 +288,8 @@ Version 1 type numerals are not a good choice for the simply-typed 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 +represented by the function `\x.x false 0`, one must have type (τ +--> τ --> &tau) --> &sigma --> σ. 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