next up previous contents
Next: Declarations and Comments Up: The Theory Environment Previous: Components of the Theory

The Syntax Lists

Use the setprecedence command to set precedence of an operator. Use the declareprefix command to set a specific default left argument for an operator; one can also declare a new unary operator with declareunary or declare an operator implicitly via the definition or proof commands as a unary operator, in which case it is automatically assigned a default left argument of defaultprefix.

The showprecs command will display all precedences, including the formally redundant left/right associativity information.

Declaration display commands will show default left arguments for operators which have them.

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