ACL2-pc::nx
(atomic macro)
move forward one argument in the enclosing term
Example and General Form:
nx
For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is x, then after executing nx, the current subterm will be
(* (- y) z).
This is the same as up followed by (dive n+1), where n is
the position of the current subterm in its parent term in the conclusion.
Thus in particular, the nx command fails if one is already at the top of
the conclusion.
Also see ACL2-pc::up, ACL2-pc::dive, ACL2-pc::top, and
ACL2-pc::bk.
