Recognize well-formed
A
(defrec tests-and-calls (tests . calls) nil)
(see the ACL2 source code)
In a well-formed
This recognizer is analogous to pseudo-tests-and-callp.
Function:
(defun pseudo-tests-and-callsp (x) (declare (xargs :guard t)) (case-match x (('tests-and-calls tests . calls) (and (pseudo-term-listp tests) (pseudo-term-listp calls))) (& nil)))