ASSERT-EVENT

assert that a given form returns a non-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.