		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-conc-info

Make-deftreeops-conc-info

Basic constructor macro for deftreeops-conc-info structures.

Syntax

(make-deftreeops-conc-info [:conc <conc>] 
                           [:discriminant-term <discriminant-term>] 
                           [:matching-thm <matching-thm>] 
                           [:check-conc-fn-equiv-thm <check-conc-fn-equiv-thm>] 
                           [:get-tree-list-list-fn <get-tree-list-list-fn>] 
                           [:rep-infos <rep-infos>])

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

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

Definition

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

Macro: make-deftreeops-conc-info

(defmacro make-deftreeops-conc-info (&rest args)
  (std::make-aggregate 'deftreeops-conc-info
                       args
                       '((:conc)
                         (:discriminant-term)
                         (:matching-thm)
                         (:check-conc-fn-equiv-thm)
                         (:get-tree-list-list-fn)
                         (:rep-infos))
                       'make-deftreeops-conc-info
                       nil))

Function: deftreeops-conc-info

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