From: Chris Barker Date: Sun, 3 Oct 2010 01:07:22 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=2ba6b449af8d0d819018bbf7c00b1ec40625b5ab edits --- diff --git a/week4.mdwn b/week4.mdwn index b7ff8790..15349c4c 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -287,7 +287,7 @@ functions, one for each type. 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 +has type τ --> τ --> τ, for some τ. Since one is represented by the function `\x.x false 0`, one must have type (τ --> τ --> τ) --> σ --> σ. But this is a different type than zero! Because each number has a different type, it becomes