nil value
Major Section: EVENTS
Examples: (assert-event (equal (+ 3 4) 7)) (assert-event (equal (+ 3 4) 7) :msg (msg "Error: ~x0" 'equal-check)) (assert-event (equal (+ 3 4) 7) :on-skip-proofs t) General Forms: (assert-event form) (assert-event form :on-skip-proofs t)
Assert-event takes a ground form, i.e., one with no free variables;
stobjs are allowed but only a single non-stobj value can be
returned. The form is then evaluated and if the result is nil, then a
so-called hard error (see er) results. This evaluation is however not done
if proofs are being skipped, as during include-book (also
see skip-proofs and see ld-skip-proofsp), unless :on-skip-proofs t is
supplied.
Normally, if an assert-event call fails then a generic failure message is
printed, showing the offending form. However, if keyword argument :msg
is supplied, then the failure message is printed as with fmt argument
~@0; see fmt. In particular, :msg is typically a string or a call
(msg str arg-0 arg-1 ... arg-k), where str is a string and each
arg-i is the value to be associated with #\i upon formatted printing
(as with fmt) of the string str.
This form may be put into a book to be certified (see books), because
assert-event is a macro whose calls expand to calls of value-triple
(see embedded-event-form). When certifying a book, guard-checking is off,
as though (set-guard-checking nil) has been evaluated;
see set-guard-checking. That, together with a ``safe mode,'' guarantees
that assert-event forms are evaluated in the logic without guard
violations while certifying a book.
