		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-rep-info

Make-deftreeops-rep-info

Basic constructor macro for deftreeops-rep-info structures.

Syntax

(make-deftreeops-rep-info [:get-tree-list-fn <get-tree-list-fn>] 
                          [:matching-thm <matching-thm>] 
                          [:get-len-fn <get-len-fn>] 
                          [:get-tree-fn <get-tree-fn>])

This is the usual way to construct deftreeops-rep-info structures. It simply conses together a structure with the specified fields.

This macro generates a new deftreeops-rep-info structure from scratch. See also change-deftreeops-rep-info, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-deftreeops-rep-info

(defmacro make-deftreeops-rep-info (&rest args)
  (std::make-aggregate 'deftreeops-rep-info
                       args
                       '((:get-tree-list-fn)
                         (:matching-thm)
                         (:get-len-fn)
                         (:get-tree-fn))
                       'make-deftreeops-rep-info
                       nil))

Function: deftreeops-rep-info

(defun deftreeops-rep-info
       (get-tree-list-fn matching-thm get-len-fn get-tree-fn)
 (declare (xargs :guard (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))))
 (declare (xargs :guard t))
 (let ((__function__ 'deftreeops-rep-info))
   (declare (ignorable __function__))
   (b* ((get-tree-list-fn
             (mbe :logic (acl2::symbol-fix get-tree-list-fn)
                  :exec get-tree-list-fn))
        (matching-thm (mbe :logic (acl2::symbol-fix matching-thm)
                           :exec matching-thm))
        (get-len-fn (mbe :logic (acl2::symbol-fix get-len-fn)
                         :exec get-len-fn))
        (get-tree-fn (mbe :logic (acl2::symbol-fix get-tree-fn)
                          :exec get-tree-fn)))
     (list (cons 'get-tree-list-fn
                 get-tree-list-fn)
           (cons 'matching-thm matching-thm)
           (cons 'get-len-fn get-len-fn)
           (cons 'get-tree-fn get-tree-fn)))))