		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::up

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

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 one level, i.e., treat the instruction as (up 1).

Also see ACL2-pc::dive, ACL2-pc::top, ACL2-pc::nx, and ACL2-pc::bk.