		Search-engine friendly clone of the ACL2 documentation.

Must-eval-to-t

A specialization of must-eval-to to ensure that a form evaluates to a non-erroneous error triple with value t.

This calls must-eval-to with t as the expr argument. Form should evaluate to an error triple (mv erp val state). If erp is nil and val is t then (must-eval-to form expr) expands to (value-triple t); otherwise expansion causes an appropriate soft error.

The keyword arguments have the same meaning as in must-eval-to.

Macro: must-eval-to-t

(defmacro
 must-eval-to-t
 (form &key (ld-skip-proofsp ':default)
       (with-output-off ':all)
       (check-expansion 'nil
                        check-expansion-p))
 (declare (xargs :guard (booleanp check-expansion)))
 (cons
  'must-eval-to
  (cons
   form
   (cons
    't
    (cons
       ':with-output-off
       (cons with-output-off
             (append (and check-expansion-p
                          (cons ':check-expansion
                                (cons check-expansion 'nil)))
                     (and (not (eq ld-skip-proofsp :default))
                          (cons ':ld-skip-proofsp
                                (cons ld-skip-proofsp 'nil))))))))))