		Search-engine friendly clone of the ACL2 documentation.

Vl-operandinfo

Change-vl-operandinfo

Modifying constructor for vl-operandinfo structures.

Syntax

(change-vl-operandinfo x 
                       [:orig-expr <orig-expr>] 
                       [:context <context>] 
                       [:prefixname <prefixname>] 
                       [:declname <declname>] 
                       [:hidtrace <hidtrace>] 
                       [:hidtype <hidtype>] 
                       [:seltrace <seltrace>] 
                       [:part <part>] 
                       [:type <type>])

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

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

(defmacro change-vl-operandinfo (x &rest args)
 (std::change-aggregate 'vl-operandinfo
                        x args
                        '((:orig-expr . vl-operandinfo->orig-expr)
                          (:context . vl-operandinfo->context)
                          (:prefixname . vl-operandinfo->prefixname)
                          (:declname . vl-operandinfo->declname)
                          (:hidtrace . vl-operandinfo->hidtrace)
                          (:hidtype . vl-operandinfo->hidtype)
                          (:seltrace . vl-operandinfo->seltrace)
                          (:part . vl-operandinfo->part)
                          (:type . vl-operandinfo->type))
                        'change-vl-operandinfo
                        'remake-vl-operandinfo))