Types

Types. Variables (replaceable symbols) have type - it is the same as non-terminal of grammar. And declaration of type is done by the following patterns:

type wff ;;
type class ;;
type set : class ;;

Here three types are declared: wff, class and set. The last type declaration binds types set and class by a chain grammar rule: class → set. This means, that you can replace any variable of type set with an expression of type class (but not in the opposite direction). Here class is called a supertype of set. You can set up any number of supertypes for a defined type:

type <t0> : <t1>, <t1>, ... , <tn> ;;