		Search-engine friendly clone of the ACL2 documentation.

Vcd-wire

Change-vcd-wire

Modifying constructor for vcd-wire structures.

Syntax

(change-vcd-wire x 
                 [:name <name>] 
                 [:msb <msb>] 
                 [:lsb <lsb>] 
                 [:code <code>])

This is an often useful alternative to make-vcd-wire.

We construct a new vcd-wire 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-vcd-wire

(defmacro change-vcd-wire (x &rest args)
  (std::change-aggregate 'vcd-wire
                         x args
                         '((:name . vcd-wire->name)
                           (:msb . vcd-wire->msb)
                           (:lsb . vcd-wire->lsb)
                           (:code . vcd-wire->code))
                         'change-vcd-wire
                         'nil))