edits

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