		Search-engine friendly clone of the ACL2 documentation.

Svex-select-part

Change-svex-select-part

Modifying constructor for svex-select-part structures.

Syntax

(change-svex-select-part x 
                         [:lsb <lsb>] 
                         [:width <width>] 
                         [:subexp <subexp>])

This is an often useful alternative to make-svex-select-part.

We construct a new svex-select-part 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-svex-select-part

(defmacro change-svex-select-part (x &rest args)
  (std::change-aggregate 'svex-select-part
                         x args
                         '((:lsb . svex-select-part->lsb)
                           (:width . svex-select-part->width)
                           (:subexp . svex-select-part->subexp))
                         'change-svex-select-part
                         'remake-svex-select-part))