		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-rep-info

Change-deftreeops-rep-info

Modifying constructor for deftreeops-rep-info structures.

Syntax

(change-deftreeops-rep-info x 
                            [: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 an often useful alternative to make-deftreeops-rep-info.

We construct a new deftreeops-rep-info structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-deftreeops-rep-info

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