With-guard-checking-event
Suppress or enable guard-checking for an event form
See documentation on the closely related utility, with-guard-checking, for relevant background.
General Forms:
(with-guard-checking-event val form)
(with-guard-checking-event (quote val) form)
where val is a legal guard-checking value (see set-guard-checking, or evaluate *guard-checking-values* to see the list
of such values), and form is a form that returns an error-triple,
(mv erp val state). This macro is identical to with-guard-checking-error-triple, except that the first argument of a call of
with-guard-checking-event must be a constant as described above, and it
will generate a legal event form embedded-event-form. For example, the
following (uninteresting) form may be placed in a book.
(with-guard-checking-event
:none
(make-event (prog2$ (car 3) '(defun f (x) x))))
In raw Lisp, (with-guard-checking-event x y) macroexpands to y;
thus, wrapping an event with with-guard-checking-event has effect only
inside the ACL2 read-eval-print loop. Because of that behavior, calls of
with-guard-checking-event must not be used in function definitions; use
with-guard-checking-error-triple in such cases.
