restricting the domain of a function

The ACL2 system provides a mechanism for restricting a function definition to a particular domain. Although such restrictions, which are called ``guards,'' are actually ignored by the ACL2 logic, they can be useful as a specification device or as a means of causing the execution of definitions directly in Common Lisp. To make such a restriction, use the :guard xarg to defun. See xargs for a discussion of how to use :guard. 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.