#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
#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,