		Search-engine friendly clone of the ACL2 documentation.

Vl-delta

Change-vl-delta

Modifying constructor for vl-delta structures.

Syntax

(change-vl-delta x 
                 [:nf <nf>] 
                 [:vardecls <vardecls>] 
                 [:assigns <assigns>] 
                 [:modinsts <modinsts>] 
                 [:gateinsts <gateinsts>] 
                 [:warnings <warnings>] 
                 [:addmods <addmods>])

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

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

(defmacro change-vl-delta (x &rest args)
  (std::change-aggregate 'vl-delta
                         x args
                         '((:nf . vl-delta->nf)
                           (:vardecls . vl-delta->vardecls)
                           (:assigns . vl-delta->assigns)
                           (:modinsts . vl-delta->modinsts)
                           (:gateinsts . vl-delta->gateinsts)
                           (:warnings . vl-delta->warnings)
                           (:addmods . vl-delta->addmods))
                         'change-vl-delta
                         'remake-vl-delta))