edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index 15349c4..d46981e 100644 (file)
--- 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
 
 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.
 
 finite types, there is no way to choose a type for the variable `x`
 that can satisfy all of the requirements imposed on it.