		Search-engine friendly clone of the ACL2 documentation.

Guard

Guard-quick-reference

Brief summary of guard checking and guard verification

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 ; skip raw Lisp if there is a guard violation :set-guard-checking :none ; skip guard checking entirely

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 two conditions are both met. First, foo is processed in :logic mode (either by setting mode :logic globally, or by including :mode :logic in the xargs declaration). Second, at least one of the following sub-conditions is met. Also see xargs, and see set-verify-guards-eagerness for how to change this behavior.

1. The xargs declaration specifies a :guard.

2. There is at least one type declaration (see declare).

3. The xargs declaration specifies :stobjs.

4. The xargs declaration specifies :verify-guards t.

(verify-termination foo ...)

causes guard verification of foo if foo is a function currently defined in :program mode and the criteria for guard verification of a defun form are met, as discussed above. The default defun-mode (see default-defun-mode) must be :logic, or else this event is ignored.