ACL2-PC_colon__colon_CHANGE-GOAL.html -- ACL2 Version 6.1

ACL2-PC::CHANGE-GOAL

(primitive) change to another goal.

Major Section:  PROOF-CHECKER-COMMANDS

Examples:
(change-goal (main . 1)) -- change to the goal (main . 1)
change-goal              -- change to the next-to-top goal

General Form:
(change-goal &optional goal-name end-flg)

Change to the goal with the name goal-name, i.e. make it the current goal. However, if goal-name is nil or is not supplied, then it defaults to the next-to-top goal, i.e., the second goal in the stack of goals. If end-flg is supplied and not nil, then move the current goal to the end of the goal stack; else merely swap it with the next-to-top goal. Also see documentation for cg.