		Search-engine friendly clone of the ACL2 documentation.

Vl-explicitvalueparam

Change-vl-explicitvalueparam

Modifying constructor for vl-explicitvalueparam structures.

Syntax

(change-vl-explicitvalueparam x 
                              [:type <type>] 
                              [:default <default>] 
                              [:final-value <final-value>])

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

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

(defmacro change-vl-explicitvalueparam (x &rest args)
  (std::change-aggregate
       'vl-explicitvalueparam
       x args
       '((:type . vl-explicitvalueparam->type)
         (:default . vl-explicitvalueparam->default)
         (:final-value . vl-explicitvalueparam->final-value))
       'change-vl-explicitvalueparam
       'remake-vl-explicitvalueparam))