next up previous contents
Next: Movement Commands Up: Appendix: Reference for Individual Previous: Environment Display Commands

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.


next up previous contents
Next: Movement Commands Up: Appendix: Reference for Individual Previous: Environment Display Commands

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