		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-numrange-info

Change-deftreeops-numrange-info

Modifying constructor for deftreeops-numrange-info structures.

Syntax

(change-deftreeops-numrange-info x 
                                 [:get-nat-fn <get-nat-fn>] 
                                 [:bounds-thm <bounds-thm>])

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

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

(defmacro change-deftreeops-numrange-info (x &rest args)
  (std::change-aggregate
       'deftreeops-numrange-info
       x args
       '((:get-nat-fn . deftreeops-numrange-info->get-nat-fn)
         (:bounds-thm . deftreeops-numrange-info->bounds-thm))
       'change-deftreeops-numrange-info
       'nil))