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. The general issue of guards and guard verification is
discussed in the topics listed below.