		Search-engine friendly clone of the ACL2 documentation.

Repeat-range

Change-repeat-range

Modifying constructor for repeat-range structures.

Syntax

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

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

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

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