		Search-engine friendly clone of the ACL2 documentation.

Pseudo-term-listp

A predicate for recognizing lists of term-like s-expressions

See pseudo-termp for a predicate that recognizes a term-like s-expression. The predicate pseudo-term-listp tests whether its argument is a list of those.

Function: pseudo-term-listp

(defun pseudo-term-listp (lst)
  (declare (xargs :guard t))
  (cond ((atom lst) (equal lst nil))
        (t (and (pseudo-termp (car lst))
                (pseudo-term-listp (cdr lst))))))