		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-table-value

Deftreeops-table-valuep

Recognizer for deftreeops-table-value structures.

Signature
(deftreeops-table-valuep x) → *

Definitions and Theorems

Function: deftreeops-table-valuep

(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
                              charval-info-alist event-alist call)))
    :exec
    (fty::alist-with-carsp
        x
        '(rulename-info-alist numrange-info-alist
                              charval-info-alist event-alist call)))
   (b* ((rulename-info-alist (cdr (std::da-nth 0 x)))
        (numrange-info-alist (cdr (std::da-nth 1 x)))
        (charval-info-alist (cdr (std::da-nth 2 x)))
        (event-alist (cdr (std::da-nth 3 x)))
        (call (cdr (std::da-nth 4 x))))
     (and (deftreeops-rulename-info-alistp rulename-info-alist)
          (deftreeops-numrange-info-alistp numrange-info-alist)
          (deftreeops-charval-info-alistp charval-info-alist)
          (symbol-pseudoeventform-alistp event-alist)
          (pseudo-event-formp call))))))

Theorem: consp-when-deftreeops-table-valuep

(defthm consp-when-deftreeops-table-valuep
  (implies (deftreeops-table-valuep x)
           (consp x))
  :rule-classes :compound-recognizer)