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