Major Section: ACL2-BUILT-INS
In the ACL2 logic,
(endp x) is the same as
atom, the guard for
endp requires that
x is a
cons pair or is
endp is typically used as a
termination test for functions that recur on a
argument. See guard for general information about guards.
Endp is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.