		Search-engine friendly clone of the ACL2 documentation.

Svtv-spec

Change-svtv-spec

Modifying constructor for svtv-spec structures.

Syntax

(change-svtv-spec x 
                  [:fsm <fsm>] 
                  [:cycle-phases <cycle-phases>] 
                  [:namemap <namemap>] 
                  [:probes <probes>] 
                  [:in-alists <in-alists>] 
                  [:override-test-alists <override-test-alists>] 
                  [:override-val-alists <override-val-alists>] 
                  [:initst-alist <initst-alist>])

This is an often useful alternative to make-svtv-spec.

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

(defmacro change-svtv-spec (x &rest args)
  (std::change-aggregate
       'svtv-spec
       x args
       '((:fsm . svtv-spec->fsm)
         (:cycle-phases . svtv-spec->cycle-phases)
         (:namemap . svtv-spec->namemap)
         (:probes . svtv-spec->probes)
         (:in-alists . svtv-spec->in-alists)
         (:override-test-alists . svtv-spec->override-test-alists)
         (:override-val-alists . svtv-spec->override-val-alists)
         (:initst-alist . svtv-spec->initst-alist))
       'change-svtv-spec
       'nil))