Recognizer for a true list of atoms
The predicate atom-listp tests whether its argument is a true-listp of atoms, i.e., of non-conses.
Function: atom-listp
(defun atom-listp (lst) (declare (xargs :guard t)) (cond ((atom lst) (eq lst nil)) (t (and (atom (car lst)) (atom-listp (cdr lst))))))
