With-guard-checking-error-triple
Suppress or enable guard-checking for a form
See documentation on the closely related utility, with-guard-checking, for relevant background.
Example:
; Turn off all guard-checking for the indicated calls of append and car:
(with-guard-checking-error-triple :none
(value (append 3 4)))
General Form:
(with-guard-checking-error-triple val form)
where val evaluates to 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); see error-triple. Thus,
with-guard-checking-error-triple is much like with-guard-checking, but the former is to be used if form mentions the
ACL2 state; indeed, with-guard-checking-error-triple requires
form to evaluate to an error triple. As with with-guard-checking,
form is evaluated in a context where guard-checking has been set to the
value of val, but this guard-checking setting is ignored once evaluation
passes into raw Lisp functions (see guards-and-evaluation).
Also see with-guard-checking-event for a similar utility to be used
for creating events, specifically, embedded-event-forms.
