		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))))))