pseudo-tests-and-calls-listp

(in-package "ACL2")

(defsection pseudo-tests-and-calls-listp
  :parents (system-utilities-non-built-in)
  :short "Recognize true lists of well-formed @('tests-and-calls') records."
  (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)))))))