Restricting the domain of a function
NOTE: Novices are often best served by avoiding guards.
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. Moreover, the guard has NO EFFECT on the proof that a recursive definition is admissible — informally, that it terminates). (See mbt for a discussion of one way to use the guard explicitly to assist with that proof while avoiding execution overhead.)
Guards can be useful as a specification device or for increasing execution
efficiency. To make such a restriction, use the
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.