ACL2-PC::WRAP1

(primitive) combine goals into a single goal 
Major Section:  PROOF-CHECKER-COMMANDS


Examples:
; Keep (main . 1) and (main . 2) if they exist, as well as the current goal;
; and for each other goal, conjoin it into the current goal and delete it:
(wrap1 ((main . 1) (main . 2)))


; As explained below, conjoin all subsequent siblings of the current goal
; into the current goal, and then delete them:
(wrap1)


General Form:
(wrap1 &optional kept-goal-names)
If kept-goal-names is not nil, the current goal is replaced by conjoining it with all goals other than the current goal and those indicated by kept-goal-names, and those other goals are deleted. If kept-goal-names is omitted, then the the current goal must be of the form (name . n), and the goals to conjoin into the current goal (and delete) are those with names of the form (name . k) for k >= n.

NOTE: Wrap1 always ``succeeds'', even if there are no other goals to conjoin into the current goal (a message is printed in that case), and it always leaves you with no hypotheses at the top of the current goal's conclusion (as though top and demote had been executed, if necessary).

Also see proof-checker documentation for wrap (see proof-checker-commands).