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.