		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-rep-info

Deftreeops-rep-infop

Recognizer for deftreeops-rep-info structures.

Signature
(deftreeops-rep-infop x) → *

Definitions and Theorems

Function: deftreeops-rep-infop

(defun deftreeops-rep-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'deftreeops-rep-infop))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(matching-thm get-tree-list-fn get-tree-fn)))
          :exec (fty::alist-with-carsp
                     x
                     '(matching-thm get-tree-list-fn get-tree-fn)))
     (b* ((matching-thm (cdr (std::da-nth 0 x)))
          (get-tree-list-fn (cdr (std::da-nth 1 x)))
          (get-tree-fn (cdr (std::da-nth 2 x))))
       (and (common-lisp::symbolp matching-thm)
            (common-lisp::symbolp get-tree-list-fn)
            (common-lisp::symbolp get-tree-fn))))))

Theorem: consp-when-deftreeops-rep-infop

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