Recognizer for abnf::tree-list-tuple2 structures.
(abnf::tree-list-tuple2p abnf::x) → *
Function:
(defun abnf::tree-list-tuple2p (abnf::x) (declare (xargs :guard t)) (let ((__function__ 'abnf::tree-list-tuple2p)) (declare (ignorable __function__)) (and (mbe :logic (and (alistp abnf::x) (equal (strip-cars abnf::x) '(1st 2nd))) :exec (fty::alist-with-carsp abnf::x '(1st 2nd))) (b* ((1st (cdr (std::da-nth 0 abnf::x))) (2nd (cdr (std::da-nth 1 abnf::x)))) (and (abnf::tree-listp 1st) (abnf::tree-listp 2nd))))))
Theorem:
(defthm abnf::consp-when-tree-list-tuple2p (implies (abnf::tree-list-tuple2p abnf::x) (consp abnf::x)) :rule-classes :compound-recognizer)