		Search-engine friendly clone of the ACL2 documentation.

Good-atom-listp

Recognizer for a true list of ``good'' atoms

The predicate good-atom-listp tests whether its argument is a true-listp of ``good'' atoms, i.e., where each element is a number, a symbol, a character, or a string.

Also see atom-listp.

Function: good-atom-listp

(defun good-atom-listp (lst)
       (declare (xargs :guard t))
       (cond ((atom lst) (eq lst nil))
             (t (and (or (acl2-numberp (car lst))
                         (symbolp (car lst))
                         (characterp (car lst))
                         (stringp (car lst)))
                     (good-atom-listp (cdr lst))))))