Declaration Commands:

It is useful to note that variable operators can be assigned relative types, strict prefix status and/or opacity using the operator declaration commands.

declaretypedinfix:

This command takes three arguments, two integers followed by a string. The string argument is declared as an operator (if it has the correct form and is not already declared) with the left type and right type indicated by the first and second integer arguments, respectively.

declareinfix:

This command takes a single string argument. The string is declared as an operator (if possible) and assigned left type and right type of 0.

declareopaque:

This command takes a single string argument. The string is declared as an opaque operator, if of the correct form and not already declared.

declareprefix:

This command takes two string arguments. The first is intended to be an infix operator (already declared) and the second a constant or numeral. The operator argument is overloaded as a prefix operator, with the second argument serving as the default left argument of terms built with the operator as a prefix.

declaretypedunary:

This command takes an integer argument and a string argument. The string is declared as a strict prefix operator, if it is of the correct form and has not already been declared, with right type determined by the integer argument. dtu is an abbreviation for declaretypedunary.

declareunary:

This command takes a single string argument. The string is declared as a strict prefix operator, if it is of the correct form and has not already been declared, with right type 0. du is an abbreviation for declareunary.

declareunaryopaque:

This command takes a single string argument. The string is declared as an opaque strict prefix operator, if it is of the right form and has not already been declared.

defaulttypeinfo:

This command takes two string arguments, a free variable and a constant. The ``default type'' of the free variable is set to the constant: this has the effect that the : operator may be used as a prefix before that variable, and the type retraction will be understood. dti is an abbreviation for defaulttypeinfo.

notypeinfo:

This command takes a single string argument, a free variable. Any default type assigned to that free variable is cancelled. nti is an abbreviation for notypeinfo.

declareconstant:

This command takes a single string argument, a constant. The argument is declared as an atomic constant term, if it is of the right form and has not already been declared.

declarepretheorem:

This command takes a single string argument, a constant or operator. The argument is declared as a ``pretheorem'' (the intention is signalled that a theorem with this name will eventually be proved), as long as it is of the correct form and has not already been declared. dpt is an abbreviation for declarepretheorem.

declareunarypretheorem:

This command takes a single string argument, an operator. The argument is declared as a pretheorem and as strict prefix, as long as it is of the correct form and has not already been declared. dupt is an abbreviation for declareunarypretheorem.

makescin:

This command takes two string arguments, an operator and a theorem. The operator is declared ``scin'' if the theorem is of the correct form.

makescinleft, makescinright:

As makescin, but the operator is declared ``scinleft'' or ``scinright'' as appropriate.

makescout:

This command takes two string arguments, an operator and a theorem. The operator is declared ``scout'' if the theorem is of the correct form.

makescinvar:

This command takes a single string argument, an operator variable, which is made ``scin''. The uses of this are technical and may be obsolete.

setprogram:

This command takes two string arguments. The first is the name of a function or operator. The second is the ``functional program'' to be bound to that function or operator.

deprogram:

This command takes one string argument. It is the name of a function or operator from which any ``functional program'' is to be unbound.