next up previous contents
Next: Declarations Up: The Internal Language Previous: Compound Terms

Navigation within Terms

The basic concept here is that each non-atomic term has a left and right subterm. The left and right subterms of a variable binding context are the same largest proper subterm. The left subterm of a term with a top-level prefix operator is the default left argument associated with that operator (it will be displayed in both local and global displays if it becomes the selected subterm).

The user sees the whole right term of the current version of the equation being proved, and sees the selected subterm as well. In the display of the entire term, the selected subterm is enclosed in braces { }. Braces are not currently used in any other way by the prover.

The basic movement commands are up, which changes the selected subterm to the smallest subterm having the current selected subterm as a proper subterm, left and right, which change the selected subterm to its left or right subterm, respectively, and top, which sets the selected subterm to the whole subterm.

More sophisticated movement commands, upto, downtoleft, and downtoright, move to remote subterms matching a term argument. New commands listed in the first command reference section below allow one to search for instances of left and right sides of theorems.

The simplest rewriting commands, applythm and applyconvthm, allow one to apply an equation whose name is given as an argument to the selected subterm. The choice of command determines whether the left or right side of the equation is matched to the selected subterm. These commands do not invoke the tactic interpreter; no automatic rewriting takes place. New commands applyenv and applyconvenv allow similar use of saved environments.

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