X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=d46981e0d7861e35f8df1006c83ab144788a64f1;hp=15349c4cffee0c16ff565284fc13870c6ee07d7e;hb=014db35e12f61a3192007298c2db56b5843f79d1;hpb=2ba6b449af8d0d819018bbf7c00b1ec40625b5ab

diff --git a/week4.mdwn b/week4.mdwn
index 15349c4c..d46981e0 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -270,9 +270,9 @@ cannot have a type in Λ_T.  We can easily see why:
 
 Assume Ω has type τ, and `\x.xx` has type σ.  Then
 because `\x.xx` takes an argument of type σ and returns
-something of type τ, `\x.xx` must also have type `σ -->
-τ`.  By repeating this reasoning, `\x.xx` must also have type
-`(σ --> τ) --> τ`; and so on.  Since variables have
+something of type τ, `\x.xx` must also have type σ -->
+τ.  By repeating this reasoning, `\x.xx` must also have type
+(σ --> τ) --> τ; and so on.  Since variables have
 finite types, there is no way to choose a type for the variable `x`
 that can satisfy all of the requirements imposed on it.