Recognizer for deftreeops-table-value structures.
(deftreeops-table-valuep x) → *
Function:
(defun deftreeops-table-valuep (x) (declare (xargs :guard t)) (let ((__function__ 'deftreeops-table-valuep)) (declare (ignorable __function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(rulename-info-alist numrange-info-alist))) :exec (fty::alist-with-carsp x '(rulename-info-alist numrange-info-alist))) (b* ((rulename-info-alist (cdr (std::da-nth 0 x))) (numrange-info-alist (cdr (std::da-nth 1 x)))) (and (deftreeops-rulename-info-alistp rulename-info-alist) (deftreeops-numrange-info-alistp numrange-info-alist))))))
Theorem:
(defthm consp-when-deftreeops-table-valuep (implies (deftreeops-table-valuep x) (consp x)) :rule-classes :compound-recognizer)