Movement Commands

right

Changes current subterm to right subterm of previous current subterm. Takes the immediate proper subterm of a constant function term (walk command ``r'').

left

Changes current subterm to left subterm of previous current subterm. Takes the immediate proper subterm of a constant function term (walk command ``l'').

up

Changes current subterm to the smallest subterm properly including the previous current subterm (walk command ``u'').

top

Changes current subterm to the whole term (walk command ``t'').

upto

``upto term'' repeats ``up'' until a term is encountered which matches ``term'' in structure, or until the whole term is reached. (walk command ``o'')

downtoleft

``downtoleft term'' goes to the leftmost term matching ``term'' in structure. (walk command ``<'')

downtoright

As ``downtoleft'', except rightmost. (walk command ``>'')

New movement commands:

Commands uptols <theorem>, uptors <theorem>, dlls <theorem>, dlrs <theorem>, drrs <theorem>, and dlrs <theorem> enable movement to places where theorems can be applied. Commands beginning with upto- implement ``upto''; commands beginning with dr- and dl- implement ``downtoleft'' and ``downtoright''; the suffix indicates ``left side'' or ``right side'' of theorem.