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
Fri Sep 5 16:28:58 MDT 1997