edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index 9175c4a..b7ff879 100644 (file)
--- 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
 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 (τ
+--> τ --> τ) --> σ --> σ.  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
 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