X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=b7ff879082a8bb7f11fe2907df3a59ed908977e1;hp=9175c4aeaf9d478cec36e04ce49ef7ad88965261;hb=6dffa91feff41dc4736d907bf59c3a76a3c8d50f;hpb=4acb0dcfac415c233c70e3125e333e07fa51a387

diff --git a/week4.mdwn b/week4.mdwn
index 9175c4ae..b7ff8790 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 (τ
+--> τ --> τ) --> σ --> σ.  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