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.