edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index ca6eb4c..15349c4 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -287,9 +287,9 @@ 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`
 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 (τ
 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
 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