Navigation Commands

These commands help the user to select the subterm of the right side of the equation under construction to which rewrite rules will be applied.

right, left:

These commands take a unit argument. They change the selected subterm to the right or left subterm (respectively) of the current subterm. Terms with a top-level strict prefix operator do not have a left subterm; an error will be reported. Case expressions do not have a right subterm; the apparent right subterm (a pair) can be viewed and moved through, but not rewritten (and will not be highlighted with braces in the display of the whole term). Abstraction (bracketed) terms are considered to have their immediate subterm as both left and right subterm.

up:

This command takes a unit argument. It changes the selected subterm, if it is not the entire right side of the equation under construction, to the smallest term which properly contains it (its parent). The up command may need to be used repeatedly to recover from subterm error conditions.

top:

This command takes a unit argument. It changes the selected subterm to the entire right side of the equation under construction.

upto, uptols, uptors:

Each of these commands takes a single string argument. upto causes the selected subterm to be the smallest term properly containing the currently selected subterm which matches its argument (a term). uptols and uptors have the name of a theorem as their argument: they cause the selected subterm to be the smallest term properly containing the currently selected subterm which matches the left or right side (respectively) of the theorem named by their argument. ut is an abreviation for upto.

downtoleft, dlls, dlrs:

Each of these commands takes a single string argument. downtoleft causes the selected subterm to be the leftmost subterm of the currently selected subterm matching its argument which contains no proper subterm matching its argument. dlls and dlrs take the name of a theorem as their argument, and have the effect of downtoleft with the left or right side (respectively) of the named theorem as its argument. dtl is an abbreviation for downtoleft.

downtoright, drls, drrs:

Exactly as the previous commands except that they look for rightmost terms. dtr is an abbreviation for downtoright.

litupto, litdowntoleft, litdowntoright:

As upto, downtoleft, downtoright, except that one moves to a term literally identical to the argument rather than one matching the argument in structure. lut, ldtl, ldtr abbreviate these commands.