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