From f4e64dfd73d6935c7636a1f4586b7d5202a74272 Mon Sep 17 00:00:00 2001
From: Chris Barker
Date: Sat, 2 Oct 2010 21:01:20 -0400
Subject: [PATCH] edits
---
week4.mdwn | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/week4.mdwn b/week4.mdwn
index 1f52cf3b..8714eae8 100644
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -217,7 +217,7 @@ and so on.
#Typed lambda terms#
-Given a set of types `T`, we define the set of typed lambda terms `Λ~T~`

,
+Given a set of types `T`, we define the set of typed lambda terms `Λ_T`

,
which is the smallest set such that
* each type `t` has an infinite set of distinct variables, {x^t}_1,
@@ -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 `λ a M`

has type σ --> τ.
The definitions of types and of typed terms should be highly familiar
-to semanticists, except that instead of writing `σ --> τ`,
-linguists (following Montague, who followed Church) write `<σ,
-τ>`. We will use the arrow notation, since it is more iconic.
+to semanticists, except that instead of writing σ --> τ,
+linguists (following Montague, who followed Church) write <σ,
+τ>. We will use the arrow notation, since it is more iconic.
Some examples (assume that `x` has type `o`):
--
2.11.0