		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)
           '(get-tree-list-fn matching-thm get-len-fn get-tree-fn)))
    :exec
    (fty::alist-with-carsp
         x
         '(get-tree-list-fn matching-thm get-len-fn get-tree-fn)))
   (b* ((get-tree-list-fn (cdr (std::da-nth 0 x)))
        (matching-thm (cdr (std::da-nth 1 x)))
        (get-len-fn (cdr (std::da-nth 2 x)))
        (get-tree-fn (cdr (std::da-nth 3 x))))
     (and (common-lisp::symbolp get-tree-list-fn)
          (common-lisp::symbolp matching-thm)
          (common-lisp::symbolp get-len-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)