		Search-engine friendly clone of the ACL2 documentation.

System-utilities-non-built-in

Pseudo-tests-and-calls-listp

Recognize true lists of well-formed tests-and-calls records.

Definitions and Theorems

Function: pseudo-tests-and-calls-listp

(defun pseudo-tests-and-calls-listp (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
        (t (and (pseudo-tests-and-callsp (car x))
                (pseudo-tests-and-calls-listp (cdr x))))))