next up previous contents
Next: Relative Type and Stratification Up: The Internal Language Previous: Navigation within Terms


Certain symbols need to be declared. If undeclared identifiers appear, the term entered will be parsed, but an error message will be displayed. Declarations occur automatically when some operations (such as proving theorems or making definitions) are executed.

Atomic constants, other than numerals, need to be declared. Free variables and bound variables do not need to be declared. The declareconstant command is used.

constant operators:
Non-variable operators need to be declared. An operator can be declared as unary, in which case it receives a default left argument of defaultprefix automatically (but can still be used as a binary infix!); an operator can also be assigned a specific default left argument, which must always be an atomic constant or numeral. An operator always has two integers associated with it, its ``left type'' and ``right type'', whose role in defining the notion of relative type will be discussed below. Operators can be declared with given left and right types or with the default values of 0 for both. The declareinfix or declaretypedinfix command is used.

free variable operators:
Free variable operators do not need to be declared unless it is desired that a left and right type be associated with them, in which case a declaration is necessary. The same commands are used as for constant operators. An operator variable with declared types will match only operators with the same types; an operator variable without declared types will match any operator. The declareopaque command can be used to block an untyped operator variable from being declared with a type later.

There are various kinds of special declaration which will be discussed elsewhere.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997