Display Commands

versiondate:

This command takes a unit argument. It displays the date of the current version of Watson.

speakup:

This command takes a unit argument. It resets the verbosity of the prover to normal; use it if the prover is not displaying terms normally. It is probably better to use the reset command if one has broken out of a script using Control-C.

setline:

This command takes a single integer argument. It resets the right margin for the pretty-printing functions of the prover. The default is 50. A thorough analysis of term structure can be obtained by setting the right margin to 0.

setnopause:

This command takes a unit argument and turns off the condition of the prover (normal in scripts but not in user interaction) which causes it to pause when it issues error messages (it would usually be used when the user has broken out of a script using Control-C; it is better to use the reset command in this case).

diagnostic:

This command takes a unit argument. It is a toggle: it turns on or off the condition which causes the prover to echo command lines in scripts (the default state is for there to be no echo).

envname:

This command takes a unit argument. It displays the name of the current environment (theorem under construction); this is often the null string.

theoryname:

This command takes a unit argument. It displays the name of the current theory.

theorysize:

This command takes a unit argument. It displays the number of theorems in the current theory.

look:

This command takes a unit argument. It displays the right side of the equation under construction and the selected subterm. The selected subterm is set off with braces in the display of the entire term, unless it is the virtual right hand subterm of a case expression.

lookhere:

This command takes a unit argument. It displays the selected subterm.

lookback:

This command takes a unit argument. It displays the left side of the equation under construction.

termprompts:

This command takes a unit argument. It turns on or off the prompts attached to term displays.

localdisplayoff, globaldisplayoff:

These commands take a unit argument. They turn off the local or global display output by the look command (and turn on the other).

bothdisplays:

This command takes a unit argument. It restores both term displays in the look command.

showdec:

This command takes a single string argument, the name of a constant or operator. It displays declaration information about its argument.

thmdisplay:

This command takes a single string argument, which should be the name of a theorem. It displays the theorem named by its argument (or issues an error message). td is an abbreviation for thmdisplay.

showenv:

As thmdisplay but displays saved environments.

tacticdisplay:

As thmdisplay, but argument may be a tactic with parameter list.

showmatchtheorem:

This command takes two string arguments, the left and right sides of a proposed equation. A theorem justifying the proposed equation is displayed, if there is one. smt is an abbreviation for showmatchtheorem.

seeprogram:

This command takes one string argument, the name of a function or operator. The ``functional program'' bound to that operator is displayed.

showdef:

This command takes a single string argument, the name of a constant or operator. It displays definition information about its argument.

showscin, showscout:

These commands take a single string argument, the name of a constant or operator. The theorem (or possibly two theorems in the case of showscin) witnessing the scin or scout character of the operator or constant will be displayed.

lookhyps:

This command displays the hypotheses of case expressions which can be used for rewriting the selected subterm. It also displays the index of the highest ``locally free'' bound variable. In general terms, it displays all context-dependent information.

seedeps:

This command takes a unit argument. It displays the axiomatic dependencies of the equation under construction.

showalldeps:

This command takes a single string argument, the name of a theorem. It displays all dependencies (axiomatic, definition, and theorem text) of the theorem named by its argument.

whatuses:

This command takes a single string argument, the name of a theorem. It displays all theorems which have theorem text dependencies on the theorem named by its argument: these are the theorems which would be forgotten or exported if the theorem named by the argument were forgotten or exported.

showalltheorems:

This command takes a unit argument. It displays all theorems, one at a time. Enter ; to continue or e; to stop (return to continue and q to stop in old versions). Theorems are displayed in alphabetical order. sat is an abbreviation for showalltheorems.

showrelevantthms:

This command takes a unit argument. It displays all theorems whose left or right side matches the currently selected subterm, excluding certain extremely generic forms for the left or right side (such as a free variable). It displays them one at a time; see showalltheorems for details. srt is an abbreviation for showrelevantthms.

showmodule:

This command takes a single string argument, the name of a theorem. It will show the theorems in the module associated with that theorem. In format it is similar to showalltheorems.

showaxioms:

This command takes a unit argument. It displays all axioms and definitions (one at a time: see showalltheorems for details).

showview:

This command takes a single string argument, the name of a view. It displays the view in a tabular format.

showprograms:

This command takes a unit argument. It shows the ``functional programming'' bindings of theorems to constants and operators in a tabular format.

statementdisplay:

This command takes a unit argument. It turns on and off a special form of display for ``statements'' (theorems with right side true) and ``converse statements'' (theorems with left side true).

setprecedence:

This command takes a string argument followed by an integer argument. The operator named by the string is assigned the precedence for purposes of parsing determined by the integer argument. Operators with even precedence group to the right and operators with odd precedence group to the left.

setdefaultprec:

This command takes an integer argument. This command sets the default precedence for operators not explicitly assigned precedences. This is 0 if setdefaultprec is not used.

sameprec:

This command takes two string arguments, interpreted as operators. The precedence of the second is set to be the same as the precedence of the first. This command and the commands under the next two headings make it unnecessary ever to refer to a precedence numerically.

defaultprecsame:

This command takes one string argument, interpreted as an operator. The default precedence is set to the precedence of the argument.

leftprecabove, leftprecbelow, rightprecabove, rightprecbelow

: Each of these commands takes two string arguments, interpreted as operators. The precedence of the second is set to group to left or right as appropriate (from the name of the command used) and to be just stronger than (above) or just weaker than (below) the precedence of the second operator. Global shifts in the numerical representation of other precedences occur.

clearprecs:

This command takes a unit argument. The command resets all precedences to 0 (the default state of the prover).

compress, expand:

Each of these commands takes a unit argument. compress compresses the display format vertically (reducing the number of carriage returns used); expand restores the default display format.