Filtering...

must-eval-to-t

books/std/testing/must-eval-to-t

Included Books

must-eval-to
other
(in-package "ACL2")
include-book
(include-book "must-eval-to")
other
(defxdoc must-eval-to-t
  :parents (std/testing errors must-eval-to)
  :short "A specialization of @(tsee must-eval-to) to ensure that
          a form evaluates to a non-erroneous error triple with value @('t')."
  :long "<p>This calls @(tsee 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.</p>

   <p>The keyword arguments have the same meaning
   as in @(tsee must-eval-to).</p>

   @(def must-eval-to-t)")
must-eval-to-tmacro
(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)))
  `(must-eval-to ,FORM
    t
    :with-output-off ,WITH-OUTPUT-OFF
    ,@(AND CHECK-EXPANSION-P `(:CHECK-EXPANSION ,CHECK-EXPANSION))
    ,@(AND (NOT (EQ LD-SKIP-PROOFSP :DEFAULT)) `(:LD-SKIP-PROOFSP ,LD-SKIP-PROOFSP))))