We describe the syntax of the input language. Tokens are either identifiers (made of alphanumeric characters and the characters ``_" and ``?") or operators (made up of special characters, excluding parentheses, quotes, braces, and brackets).
Identifiers have two special subsets: numerals (all characters numeric) and variables (starting with ``?"). Other identifiers are called ``constants". Operators starting with a caret are operator variables and an initial colon represents an operation on operators which may be iterated.
Constants and operators other than variables must be declared to be used. Predeclared constants include ``RAISE" (a built-in theorem), ``true" and ``false". Built-in operators include ``=", ``," (pairing), ``@" (function application), ``=>", ``=>>", ``<=", and ``<<=" (theorem embedding infixes), ``+!", ``*!", ``-!", ``/!", ``%!", ``=!", and ``<!" (operators of the built-in unsigned integer arithmetic).
Single identifiers of whatever class are terms. Any term enclosed in parentheses is a term. A term preceded by an operator (here used as a unary prefix) is a term. An operator flanked by terms is a term (here the operator is used as an infix). A term enclosed in brackets is a term (a constant function whose value is the enclosed term).
In the current version, each operator used as a prefix has associated with it a default left argument (selected by the user). In other words, all unary prefix terms are abbreviations for binary infix terms. If an operator for which a default left argument has not been declared is used as a prefix, a bogus value is used which signals an error condition to the prover. It should be noted that the ``left" movement command can for this reason be used with prefix terms. The declareunary command above should be used for prefixes which are not also to be used as infixes; the declareprefix command below can be used to set desired behavior where overloading is intended.
The default operator precedence assigns to all infixes and prefixes the same precedence and associates to the right as far as possible. The user can assign integer precedences to prefixes/infixes (and this information can be stored in theories); higher precedences bind more tightly; even precedence associates to the right and odd to the left.
Two lists are used by the parser and are actually components of the theory type: PREFIXINFO contains operators with default left arguments and PRECEDENCEINFO contains precedence information. Saved theories are actually stored in default precedence in the current version, and the precedence list is loaded at the end of the process. Parsing is done in a first pass independent of declaration checking; the parser will parse and display terms which the prover will tell you contain undeclared constants or operators.
There is some pretty-printing built into the prover's display function; some indenting is done in a way which is intended to suggest the structure of terms. There are commands to set the right margin of the display and to set the ``depth" of the display.
Commands which relate to term display include: