Assert!
Event variant of assert$ that abbreviates assert-event
The assert! macro is similar to assert$, in that both
check that a given form evaluates to a non-nil value. However, calls of
assert! may appear as top-level events in books and encapsulate forms. Indeed, calls of assert! directly abbreviate
corresponding calls of the built-in event macro, assert-event.
You may find it more convenient to use assert-event, which has more
options. In particular, with assert-event the assertion need not return
a single, non-stobj value.
See assert$ and assert* for assertion-checking utilities to
use in programs.
Example Forms:
(assert! (equal 3 3))
(assert! (null (@ ld-skip-proofsp)))
(assert! (equal 3 3)
(defun f (x) (cons x x)))
General Forms:
(assert! assertion)
(assert! assertion event)
where assertion evaluates to a single non-stobj value and
event, if supplied and non-nil, is an event to be evaluated
if the value of assertion is not nil. It is an error if that value
is nil. As noted above, a call of assert! is an event: it
can go into a book or an encapsulate or progn event.
Calls of assert! skip evaluation of the given assertion when proofs
are being skipped: during include-book, during the second pass of an
encapsulate event, and after evaluating (set-ld-skip-proofsp t
state).
The two General Forms above may be expressed, respectively, in terms of the
more flexible built-in event macro, assert-event, as follows.
See assert-event for more detailed documentation.
(assert-event assertion
:ctx ''assert!)
(assert-event assertion
:event event
:ctx ''assert!)
