		Search-engine friendly clone of the ACL2 documentation.

Svtv

Change-svtv

Modifying constructor for svtv structures.

Syntax

(change-svtv x 
             [:name <name>] 
             [:outexprs <outexprs>] 
             [:nextstate <nextstate>] 
             [:states <states>] 
             [:inmasks <inmasks>] 
             [:outmasks <outmasks>] 
             [:inmap <inmap>] 
             [:orig-ins <orig-ins>] 
             [:orig-overrides <orig-overrides>] 
             [:orig-outs <orig-outs>] 
             [:orig-internals <orig-internals>] 
             [:expanded-ins <expanded-ins>] 
             [:expanded-overrides <expanded-overrides>] 
             [:nphases <nphases>] 
             [:labels <labels>] 
             [:form <form>])

This is an often useful alternative to make-svtv.

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

(defmacro change-svtv (x &rest args)
  (std::change-aggregate
       'svtv
       x args
       '((:name . svtv->name)
         (:outexprs . svtv->outexprs)
         (:nextstate . svtv->nextstate)
         (:states . svtv->states)
         (:inmasks . svtv->inmasks)
         (:outmasks . svtv->outmasks)
         (:inmap . svtv->inmap)
         (:orig-ins . svtv->orig-ins)
         (:orig-overrides . svtv->orig-overrides)
         (:orig-outs . svtv->orig-outs)
         (:orig-internals . svtv->orig-internals)
         (:expanded-ins . svtv->expanded-ins)
         (:expanded-overrides . svtv->expanded-overrides)
         (:nphases . svtv->nphases)
         (:labels . svtv->labels)
         (:form . svtv->form))
       'change-svtv
       'nil))