Endp
Recognizer for empty lists
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.
Function: endp
(defun endp (x)
(declare (xargs :guard (or (consp x) (eq x nil))))
(atom x))
