Guards

Common Lisp functions are partial; they are not defined for all
possible inputs. But ACL2 functions are total. Roughly speaking, the logical
function of a given name in ACL2 is a **completion** of the Common Lisp
function of the same name obtained by adding some arbitrary but ``natural''
values on arguments outside the ``intended domain'' of the Common Lisp
function.

ACL2 requires that every ACL2 function symbol have a ``guard,'' which may
be thought of as a predicate on the formals of the function describing the
intended domain. The guard on the primitive function `car`

**But guards are entirely extra-logical**: they are not involved in the
axioms defining functions. If you put a guard on a defined function, the
defining axiom added to the logic defines the function on **all**
arguments, not just on the guarded domain.

So what is the purpose of guards?

The key to the utility of guards is that we provide a mechanism, called ``guard verification,'' for checking that all the guards in a formula are true. See verify-guards. This mechanism will attempt to prove that all the guards encountered in the evaluation of a guarded function are true every time they are encountered.

For a thorough discussion of guards, see the paper [km97] in the ACL2 bibliography.