		Search-engine friendly clone of the ACL2 documentation.

Vl-hidstep

Change-vl-hidstep

Modifying constructor for vl-hidstep structures.

Syntax

(change-vl-hidstep x 
                   [:name <name>] 
                   [:index <index>] 
                   [:item <item>] 
                   [:ss <ss>] 
                   [:elabpath <elabpath>])

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

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

(defmacro change-vl-hidstep (x &rest args)
  (std::change-aggregate 'vl-hidstep
                         x args
                         '((:name . vl-hidstep->name)
                           (:index . vl-hidstep->index)
                           (:item . vl-hidstep->item)
                           (:ss . vl-hidstep->ss)
                           (:elabpath . vl-hidstep->elabpath))
                         'change-vl-hidstep
                         'remake-vl-hidstep))