ACL2-pc::wrap1
(primitive)
combine goals into a single goal
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 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 ACL2-pc::wrap.
