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