ACL2-pc::top
(atomic macro)
move to the top of the goal
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.
Also see ACL2-pc::up, ACL2-pc::dive, ACL2-pc::nx, and
ACL2-pc::bk.
