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