Modifying constructor for deftreeops-rulename-info structures.
(change-deftreeops-rulename-info x [:alt <alt>] [:nonleaf-thm <nonleaf-thm>] [:rulename-thm <rulename-thm>] [:match-thm <match-thm>] [:concs-thm <concs-thm>] [:conc-equivs-thm <conc-equivs-thm>] [:alt-kind <alt-kind>] [:check-conc-fn <check-conc-fn>] [:conc-infos <conc-infos>])
This is an often useful alternative to make-deftreeops-rulename-info.
We construct a new deftreeops-rulename-info structure that is a copy of
This is an ordinary
Macro:
(defmacro change-deftreeops-rulename-info (x &rest args) (std::change-aggregate 'deftreeops-rulename-info x args '((:alt . deftreeops-rulename-info->alt) (:nonleaf-thm . deftreeops-rulename-info->nonleaf-thm) (:rulename-thm . deftreeops-rulename-info->rulename-thm) (:match-thm . deftreeops-rulename-info->match-thm) (:concs-thm . deftreeops-rulename-info->concs-thm) (:conc-equivs-thm . deftreeops-rulename-info->conc-equivs-thm) (:alt-kind . deftreeops-rulename-info->alt-kind) (:check-conc-fn . deftreeops-rulename-info->check-conc-fn) (:conc-infos . deftreeops-rulename-info->conc-infos)) 'change-deftreeops-rulename-info 'nil))