Term-list-listp
recognizer for a list of clauses
Example:
(term-list-listp
'(((NOT (ENDP X)) (NATP (LEN X)))
((ENDP X) (NOT (NATP (LEN (CDR X)))) (NATP (LEN X))))
(w state))
General Form:
(term-list-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
true lists of quotations of well-formed terms in w.
This function is the standard ACL2 idiom for recognizing a ``set of
clauses.'' 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 to this function 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.
Function: term-list-listp
(defun term-list-listp (l w)
(declare (xargs :guard (plist-worldp-with-formals w)))
(if (atom l)
(equal l nil)
(and (term-listp (car l) w)
(term-list-listp (cdr l) w))))
