		Search-engine friendly clone of the ACL2 documentation.

Assert?

A variation of assert$ with customizable context and message.

If the optional context and message arguments are not supplied, this macro works similarly to assert$. If they are supplied and the test fails, they are used to display the hard error.

The two optional arguments must be either both supplied or both not supplied. The guard requires that.

All the arguments of this macro are evaluated. The (evaluated) context must be a symbol. The (evaluated) message must have type msgp.

Macro: assert?

(defmacro assert? (test form &optional ctx msg)
 (declare (xargs :guard (iff ctx msg)))
 (cons
  'if
  (cons
   test
   (cons
    form
    (cons
     (if msg
      (cons
       'hard-error
       (cons
        ctx
        (cons
          '"~@0"
          (cons (cons 'list
                      (cons (cons 'cons (cons '#\0 (cons msg 'nil)))
                            'nil))
                'nil))))
      (cons
       'hard-error
       (cons
        (or ctx ''assert?)
        (cons
         '"Assertion failed:~%~x0"
         (cons
          (cons
           'list
           (cons
            (cons
             'cons
             (cons
               '#\0
               (cons (cons 'quote
                           (cons (cons 'assert?
                                       (cons test (cons form 'nil)))
                                 'nil))
                     'nil)))
            'nil))
          'nil)))))
     'nil)))))