Display Control Commands

declareprefix

``declareprefix infix default'' causes the operator ``infix'' to be usable as a unary prefix, with invisible left subterm ``default'' (walk command ``X'').

deprefix

``deprefix infix'' removes any default prefix assigned to ``infix''.

setprecedence

``setprecedence infix number'' causes the operator ``infix'' to be assigned the precedence ``number'' (this parameter is not enclosed in double quotes). Non-negative integers are permitted as precedences. Odd precedences associate to the left; even precedences to the right. Precedence information is saved in saved theories; however, theorems are recorded in theory files in the old syntax. The default precedence for any operator is 0 (walk command ``I'').

showprecs

Displays precedence information in a tabular format; also gives left or right association information. (walk command ``k'')

clearprecs

Sets all precedences back to 0 (so we are back to the original precedence convention of the prover; no precedence and all operations associate to the right).

setline

``setline number'' sets the point at which lines wrap around in the display to ``number'' (the argument is not enclosed in double quotes). (walk command ``K'')

setdepth

Sets the depth of the display (terms below this depth will not be seen--they are replaced with some impossible string). The form of the command is ``setdepth number'', and the number is not enclosed in double quotes. If the number is negative (as it usually is), all subterms will be displayed.

nodepth

Sets depth to a negative value so that all subterms are displayed.

declaretypeinfo

declaretypeinfo variable type enables the term :?variable (the variable parameter is currently entered without leading ?, though this will probably be changed) to be read as type : ?variable; this allows implicit typing of variables. This information is not currently saved in theories.

detypeinfo

detypeinfo variable turns off any implicit typing of the variable ?variable.