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) :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.

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).