Term-listp
recognizer for a list of quotations of terms and of clauses
Example:
(term-listp '((ZP X) 'NIL (CONS X Y)) (w state))
General Form:
(term-listp x w)
where x is any ACL2 object and w is an ACL2 logical world.
The result is t or nil according to whether x is a true list of
quotations of well-formed terms in w.
This function is used in the definition of termp. In addition,
term-listp is the standard ACL2 idiom for recognizing a clause (``set of
literals''). See clause and see clause-processor. Each clause
processor is supposed to take a clause (i.e., term-listp) as input and
yield a list of clauses (i.e., term-list-listp) as output. When a
clause processor is run by the theorem prover its input is guaranteed to be a
well-formed clause by invariants maintained by ACL2. But its output is
checked by an explicit call of term-list-listp unless the user has
proved that the clause processor always returns a list of clauses (see well-formedness-guarantee) or has taken the risk of disabling the runtime
test with set-skip-meta-termp-checks.
Term-listp is mutually recursive with termp.
Function: term-listp
(defun term-listp (x w)
(declare (xargs :guard (plist-worldp-with-formals w)))
(cond ((atom x) (equal x nil))
((termp (car x) w)
(term-listp (cdr x) w))
(t nil)))
