GUARD.html -- ACL2 Version 3.1

GUARD

restricting the domain of a function

Major Section:  MISCELLANEOUS

The ACL2 system provides a mechanism for restricting a function definition to a particular domain. Although such restrictions, which are called ``guards,'' are actually ignored by the ACL2 logic, they can be useful as a specification device or as a means of causing the execution of definitions directly in Common Lisp. To make such a restriction, use the :guard xarg to defun. See xargs for a discussion of how to use :guard. The general issue of guards and guard verification is discussed in the topics listed below.

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.

GUARD

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