edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index 6613fb4..8714eae 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -227,12 +227,12 @@ which is the smallest set such that
      σ, then the application `(M N)` has type τ.
 
 *    If a variable `a` has type σ, and term `M` has type τ, 
-     then the abstract `λ a M` has type `σ --> τ`.
+     then the abstract <code>&lambda; a M</code> has type &sigma; --> &tau;.
 
 The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing `&sigma; --> &tau;`,
-linguists (following Montague, who followed Church) write `<&sigma;,
-&tau;>`.  We will use the arrow notation, since it is more iconic.
+to semanticists, except that instead of writing &sigma; --> &tau;,
+linguists (following Montague, who followed Church) write <&sigma;,
+&tau;>.  We will use the arrow notation, since it is more iconic.
 
 Some examples (assume that `x` has type `o`):