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. 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