previous

top

next
The usual definition of types
The set of types, T, is defined inductively:
x is in T
A, B in T implies (A>B) is in T
where x is an arbitrary variable.