		Search-engine friendly clone of the ACL2 documentation.

Vl-class

Change-vl-class

Modifying constructor for vl-class structures.

Syntax

(change-vl-class x 
                 [:name <name>] 
                 [:warnings <warnings>] 
                 [:minloc <minloc>] 
                 [:maxloc <maxloc>] 
                 [:atts <atts>] 
                 [:comments <comments>] 
                 [:virtualp <virtualp>] 
                 [:lifetime <lifetime>] 
                 [:paramdecls <paramdecls>] 
                 [:fundecls <fundecls>] 
                 [:taskdecls <taskdecls>] 
                 [:vardecls <vardecls>] 
                 [:imports <imports>] 
                 [:typedefs <typedefs>])

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

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

(defmacro change-vl-class (x &rest args)
  (std::change-aggregate 'vl-class
                         x args
                         '((:name . vl-class->name)
                           (:warnings . vl-class->warnings)
                           (:minloc . vl-class->minloc)
                           (:maxloc . vl-class->maxloc)
                           (:atts . vl-class->atts)
                           (:comments . vl-class->comments)
                           (:virtualp . vl-class->virtualp)
                           (:lifetime . vl-class->lifetime)
                           (:paramdecls . vl-class->paramdecls)
                           (:fundecls . vl-class->fundecls)
                           (:taskdecls . vl-class->taskdecls)
                           (:vardecls . vl-class->vardecls)
                           (:imports . vl-class->imports)
                           (:typedefs . vl-class->typedefs))
                         'change-vl-class
                         'remake-vl-class))