GUARD

Major Section:  MISCELLANEOUS

The ACL2 system provides a mechanism for restricting a function to a particular domain. Such restrictions are called ``guards.'' A definition's guard has no effect on the logical axiom added when that definition is accepted by ACL2, and novices are often best served by avoiding guards. However, guards can be useful as a specification device or for increasing execution efficiency. To make such a restriction, use the :guard keyword (see xargs) or, especially if you want the host Lisp compiler to use this information, use type declarations (see declare; also see xargs for a discussion of the split-types keyword). The general issue of guards and guard verification is discussed in the topics listed below.

Some Related Topics

• EXTRA-INFO -- generate markers to indicate sources of guard proof obligations

• GUARD-DEBUG -- generate markers to indicate sources of guard proof obligations

• GUARD-EVALUATION-EXAMPLES-LOG -- log showing combinations of defun-modes and guard-checking

• GUARD-EVALUATION-EXAMPLES-SCRIPT -- a script to show combinations of defun-modes and guard-checking

• GUARD-EVALUATION-TABLE -- a table that shows combinations of defun-modes and guard-checking

• GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2

• GUARD-INTRODUCTION -- introduction to guards in ACL2

• GUARD-MISCELLANY -- miscellaneous remarks about guards

• GUARD-QUICK-REFERENCE -- brief summary of guard checking and guard verification

• GUARDS-AND-EVALUATION -- the relationship between guards and evaluation

• GUARDS-FOR-SPECIFICATION -- guards as a specification device

• SET-GUARD-CHECKING -- control checking guards during execution of top-level forms

• SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.

• VERIFY-GUARDS -- verify the guards of a function

To begin further discussion of guards, see guard-introduction. That section directs the reader to further sections for more details. To see just a summary of some commands related to guards, see guard-quick-reference. For a discussion of the use of proof to verify the absence of guard violations, see verify-guards.