		Search-engine friendly clone of the ACL2 documentation.

Must-succeed*

A variant of must-succeed that accepts multiple forms.

(must-succeed* form1
               ...
               formN
               :with-output-off ...
               :check-expansion ...)

The N forms must be embedded event forms, because they are put into a progn so that earlier forms are evaluated before considering later forms in the sequence. This is a difference with must-succeed, whose form is required to return an error triple without necessarily being an embedded event form; since must-succeed takes only one form, there is no issue of earlier forms being evaluated before considering later forms as in must-succeed*.

The forms may be followed by :with-output-off and/or :check-expansion, as in must-succeed.

Macro: must-succeed*

(defmacro must-succeed* (&rest args)
 (mv-let (erp forms options)
         (partition-rest-and-keyword-args
              args
              '(:with-output-off :check-expansion))
  (if erp
   '(er
     hard? 'must-succeed*
     "The arguments of MUST-SUCCEED* must be zero or more forms ~
                followed by the options :WITH-OUTPUT-OFF and :CHECK-EXPANSION.")
   (let ((with-output-off-pair (assoc :with-output-off options))
         (check-expansion-pair (assoc :check-expansion options)))
    (cons
     'must-succeed
     (cons (cons 'progn forms)
           (append (if with-output-off-pair
                       (cons ':with-output-off
                             (cons (cdr with-output-off-pair) 'nil))
                     nil)
                   (if check-expansion-pair
                       (cons ':check-expansion
                             (cons (cdr check-expansion-pair) 'nil))
                     nil))))))))