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`

, for
example, is `(or (consp x) (equal x nil))`

, which requires the argument to
be either an ordered pair or `nil`

. We will discuss later how to specify a
guard for a defined function; when one is not specified, the guard is `t`

which is just to say all arguments are allowed.

**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.