edits

[lambda.git] / week4.mdwn

diff --git a/week4.mdwn b/week4.mdwn
index e01db2e..8fe37ad 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -192,11 +192,10 @@ are also forbidden, so recursion is neither simple nor direct.
 
 #Types#
 
 
 #Types#
 

-We will have at least one ground type, `o`.  From a linguistic
-point of view, thing of the ground types as the bar-level 0
-categories, the lexical types, such as Noun, Verb, Preposition
-(glossing over the internal complexity of those categories in modern
-theories).
+We will have at least one ground type, `o`.  From a linguistic point
+of view, think of the ground types as the bar-level 0 categories, that
+is, the lexical types, such as Noun, Verb, Preposition (glossing over
+the internal complexity of those categories in modern theories).

 
 In addition, there will be a recursively-defined class of complex
 types `T`, the smallest set such that
 
 In addition, there will be a recursively-defined class of complex
 types `T`, the smallest set such that


@@ -218,7 +217,7 @@ and so on.
 
 #Typed lambda terms#
 
 
 #Typed lambda terms#
 

-Given a set of types `T`, we define the set of typed lambda terms `&Lamda;_T`,
+Given a set of types `T`, we define the set of typed lambda terms <code>&Lamda;_T</code>,

 which is the smallest set such that
 
 *    each type `t` has an infinite set of distinct variables, {x^t}_1,
 which is the smallest set such that
 
 *    each type `t` has an infinite set of distinct variables, {x^t}_1,