ACL2-PC::TOP

(atomic macro) move to the top of the goal
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
top
For example, if the conclusion is (= x (* (- y) z)) and the current subterm is y, then after executing top, the current subterm will be the same as the conclusion, i.e., (= x (* (- y) z)).

Top is the same as (up n), where n is the number of times one needs to execute up in order to get to the top of the conclusion. The top command fails if one is already at the top of the conclusion.

See also up, dive, nx, and bk.