		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-conc-info

Change-deftreeops-conc-info

Modifying constructor for deftreeops-conc-info structures.

Syntax

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

This is an often useful alternative to make-deftreeops-conc-info.

We construct a new deftreeops-conc-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-conc-info

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