		Search-engine friendly clone of the ACL2 documentation.

Regex-repeat

Change-regex-repeat

Modifying constructor for regex-repeat structures.

Syntax

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

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

We construct a new regex-repeat 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 defprod.

Macro: change-regex-repeat

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