restricting the domain of a function

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

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.