ACL2-pc::bk
(atomic macro)
move backward one argument in the enclosing term
Example and General Form:
bk
For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is (* (- y) z), then after executing bk, the current subterm
will be x.
Move to the previous argument of the enclosing term.
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::nx.
