Major Section: GUARD
For a careful introduction to guards, see guard.
I. GUARD CHECKING DURING EXECUTION
Effect
Guards on definitions are checked at execution time (except for guards on subsidiary calls of recursive or mutually recursive functions).
When does it happen
By default, guards are checked for all forms submitted at the top level.
To disable
:set-guard-checking nil
To (re-)enable
:set-guard-checking t
See set-guard-checking for more options.
II. GUARD VERIFICATION
Effect
A proof is attempted of the obligations arising from the guards of
subsidiary functions in a defun, defthm, or defaxiom event.
In the case of a defun, the guard itself is also verified (under an
implicit guard of t).
When does it happen
Only names of defined functions, defthms, and defaxioms are
subject to guard verification. Guard verification may occur when
functions are defined (using defun), but it requires an explicit
call of verify-guards in order to verify guards for defthms
and defaxioms. Constrained functions (see encapsulate) may
not have their guards verified.
(verify-guards foo ...)
causes guard verification for the defun, defthm, or defaxiom named
by foo, if it has not already been successfully done. The default
defun-mode (see default-defun-mode) must be :logic, or else
this event is ignored.
(defun foo ...)
causes guard verification of foo if and only if the following
conditions are both met. (However,
see set-verify-guards-eagerness for how to change this
behavior.)
1. Foo is processed in:logicmode (either by setting mode:logicglobally, or by including:mode :logicin thexargsdeclaration).2. The
xargsdeclaration (see xargs) either specifies:guardor specifies:verify-guardst(or both).
(verify-termination foo ...)
causes guard verification of foo if foo is a function currently
defined in :program mode and the appropriate xargs are supplied, as
discussed for the case of defun above. The default defun-mode
(see default-defun-mode) must be :logic, or else this event is
ignored.
