ACL2-PC_colon__colon_UP.html -- ACL2 Version 3.1

ACL2-PC::UP

(primitive) move to the parent (or some ancestor) of the current subterm

Major Section:  PROOF-CHECKER-COMMANDS

Examples:  if the conclusion is (= x (* (- y) z)) and the
           current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2)       -- the current subterm becomes (* (- y) z)
(up 3)       -- the current subterm becomes the entire conclusion
(up 4)       -- no change; can't go up that many levels

General Form:
(up &optional n)

Move up n levels in the conclusion from the current subterm, where n is a positive integer. If n is not supplied or is nil, then move up 1 level, i.e., treat the instruction as (up 1).