#Typed lambda terms#
-Given a set of types `T`, we define the set of typed lambda terms <code>Λ~T~</code>,
+Given a set of types `T`, we define the set of typed lambda terms <code>Λ_T</code>,
which is the smallest set such that
* each type `t` has an infinite set of distinct variables, {x^t}_1,
σ, 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>λ a M</code> 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`):