GUARD-QUICK-REFERENCE

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

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 :logic mode (either by setting mode :logic globally, or by including :mode :logic in the xargs declaration).

2. The xargs declaration (see xargs) either specifies :guard or specifies :verify-guards t (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.