		Search-engine friendly clone of the ACL2 documentation.

Svtv*-phase

Change-svtv*-phase

Modifying constructor for svtv*-phase structures.

Syntax

(change-svtv*-phase x 
                    [:label <label>] 
                    [:inputs <inputs>] 
                    [:overrides <overrides>] 
                    [:outputs <outputs>])

This is an often useful alternative to make-svtv*-phase.

We construct a new svtv*-phase 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-svtv*-phase

(defmacro change-svtv*-phase (x &rest args)
  (std::change-aggregate 'svtv*-phase
                         x args
                         '((:label . svtv*-phase->label)
                           (:inputs . svtv*-phase->inputs)
                           (:overrides . svtv*-phase->overrides)
                           (:outputs . svtv*-phase->outputs))
                         'change-svtv*-phase
                         'nil))