introduction to guards in ACL2
Major Section:  GUARD

Most users can probably profit by avoiding dealing with guards most of the time. If they seem to get in the way, they can be ``turned off'' using the command :set-guard-checking nil; for more about this, see set-guard-checking. For more about guards in general, see guard.

The guard on a function symbol is a formula about the formals of the function. To see the guard on a function, use the keyword command :args. See args. To specify the guard on a function at defun-time, use the :guard xarg. See xargs.

Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function ``should'' have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. Briefly: If the guards of a function definition are ``verified'' (see verify-guards), then the evaluation of a call of that function on arguments satisfying its guard will have the following property:

All subsequent function calls during that evaluation will be on arguments satisfying the guard of the called function.
The consequence of this fact for (a) is that your specification function is well-formed, in the sense that the values returned by this function on appropriate arguments only depend on the restrictions of the called functions to their intended domains. The consequence of this fact for (b) is that in the ACL2 system, when a function whose guards have been verified is called on arguments that satisfy its guard, then the raw lisp function defined by this function's defun event is used to evaluate the call. Note however that even when the user-supplied defun is not used, ACL2 uses a corresponding ``executable counterpart'' that generally performs, we expect, nearly as well as the raw lisp function. See comp to see how compilation can speed up both kinds of execution.

Let us turn next to the issue of the relationship between guards and evaluation. See guards-and-evaluation.