		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-conc-info

Deftreeops-conc-infop

Recognizer for deftreeops-conc-info structures.

Signature
(deftreeops-conc-infop x) → *

Definitions and Theorems

Function: deftreeops-conc-infop

(defun deftreeops-conc-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'deftreeops-conc-infop))
  (declare (ignorable __function__))
  (and
   (mbe
      :logic (and (alistp x)
                  (equal (strip-cars x)
                         '(conc discriminant-term
                                matching-thm check-conc-fn-equiv-thm
                                get-tree-list-list-fn rep-infos)))
      :exec (fty::alist-with-carsp
                 x
                 '(conc discriminant-term
                        matching-thm check-conc-fn-equiv-thm
                        get-tree-list-list-fn rep-infos)))
   (b* ((conc (cdr (std::da-nth 0 x)))
        (?discriminant-term (cdr (std::da-nth 1 x)))
        (matching-thm (cdr (std::da-nth 2 x)))
        (check-conc-fn-equiv-thm (cdr (std::da-nth 3 x)))
        (get-tree-list-list-fn (cdr (std::da-nth 4 x)))
        (rep-infos (cdr (std::da-nth 5 x))))
     (and (concatenationp conc)
          (common-lisp::symbolp matching-thm)
          (common-lisp::symbolp check-conc-fn-equiv-thm)
          (common-lisp::symbolp get-tree-list-list-fn)
          (deftreeops-rep-info-listp rep-infos))))))

Theorem: consp-when-deftreeops-conc-infop

(defthm consp-when-deftreeops-conc-infop
  (implies (deftreeops-conc-infop x)
           (consp x))
  :rule-classes :compound-recognizer)