WITH-GUARD-CHECKING.html -- ACL2 Version 6.3

WITH-GUARD-CHECKING

suppressing or enable guard-checking for a form

Major Section:  SWITCHES-PARAMETERS-AND-MODES

Example:

; Turn off all guard-checking for the indicated calls of append and car:
(with-guard-checking :none
                     (car (append 3 4)))

General Form:
(with-guard-checking 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 to be evaluated as though we had first executed (set-guard-checking val). Of course, this gaurd-checking setting is active only during evaluation of form, and is ignored once evaluation passes into raw Lisp functions (see guards-and-evaluation).