		Search-engine friendly clone of the ACL2 documentation.

Num-range

Change-num-range

Modifying constructor for num-range structures.

Syntax

(change-num-range x 
                  [:base <base>] 
                  [:min <min>] 
                  [:max <max>])

This is an often useful alternative to make-num-range.

We construct a new num-range 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-num-range

(defmacro change-num-range (x &rest args)
  (std::change-aggregate 'num-range
                         x args
                         '((:base . num-range->base)
                           (:min . num-range->min)
                           (:max . num-range->max))
                         'change-num-range
                         'nil))