Major Section: ACL2-BUILT-INS
In the ACL2 logic, (endp x) is the same as (atom x).
See atom.
Unlike atom, the guard for endp requires that x is a
cons pair or is nil. Thus, endp is typically used as a
termination test for functions that recur on a true-listp
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.
