		Search-engine friendly clone of the ACL2 documentation.

Vl-blockscope

Change-vl-blockscope

Modifying constructor for vl-blockscope structures.

Syntax

(change-vl-blockscope x 
                      [:imports <imports>] 
                      [:paramdecls <paramdecls>] 
                      [:vardecls <vardecls>] 
                      [:typedefs <typedefs>] 
                      [:scopetype <scopetype>] 
                      [:name <name>])

This is an often useful alternative to make-vl-blockscope.

We construct a new vl-blockscope 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-vl-blockscope

(defmacro change-vl-blockscope (x &rest args)
  (std::change-aggregate 'vl-blockscope
                         x args
                         '((:imports . vl-blockscope->imports)
                           (:paramdecls . vl-blockscope->paramdecls)
                           (:vardecls . vl-blockscope->vardecls)
                           (:typedefs . vl-blockscope->typedefs)
                           (:scopetype . vl-blockscope->scopetype)
                           (:name . vl-blockscope->name))
                         'change-vl-blockscope
                         'remake-vl-blockscope))