		Search-engine friendly clone of the ACL2 documentation.

Svtv-data-obj

Change-svtv-data-obj

Modifying constructor for svtv-data-obj structures.

Syntax

(change-svtv-data-obj x 
                      [:design <design>] 
                      [:user-names <user-names>] 
                      [:namemap <namemap>] 
                      [:namemap-validp <namemap-validp>] 
                      [:flatten <flatten>] 
                      [:flatten-validp <flatten-validp>] 
                      [:flatnorm-setup <flatnorm-setup>] 
                      [:flatnorm <flatnorm>] 
                      [:flatnorm-validp <flatnorm-validp>] 
                      [:phase-fsm-setup <phase-fsm-setup>] 
                      [:phase-fsm <phase-fsm>] 
                      [:phase-fsm-validp <phase-fsm-validp>] 
                      [:cycle-phases <cycle-phases>] 
                      [:cycle-fsm <cycle-fsm>] 
                      [:cycle-fsm-validp <cycle-fsm-validp>] 
                      [:pipeline-setup <pipeline-setup>] 
                      [:pipeline <pipeline>] 
                      [:pipeline-validp <pipeline-validp>])

This is an often useful alternative to make-svtv-data-obj.

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

(defmacro change-svtv-data-obj (x &rest args)
  (std::change-aggregate
       'svtv-data-obj
       x args
       '((:design . svtv-data-obj->design)
         (:user-names . svtv-data-obj->user-names)
         (:namemap . svtv-data-obj->namemap)
         (:namemap-validp . svtv-data-obj->namemap-validp)
         (:flatten . svtv-data-obj->flatten)
         (:flatten-validp . svtv-data-obj->flatten-validp)
         (:flatnorm-setup . svtv-data-obj->flatnorm-setup)
         (:flatnorm . svtv-data-obj->flatnorm)
         (:flatnorm-validp . svtv-data-obj->flatnorm-validp)
         (:phase-fsm-setup . svtv-data-obj->phase-fsm-setup)
         (:phase-fsm . svtv-data-obj->phase-fsm)
         (:phase-fsm-validp . svtv-data-obj->phase-fsm-validp)
         (:cycle-phases . svtv-data-obj->cycle-phases)
         (:cycle-fsm . svtv-data-obj->cycle-fsm)
         (:cycle-fsm-validp . svtv-data-obj->cycle-fsm-validp)
         (:pipeline-setup . svtv-data-obj->pipeline-setup)
         (:pipeline . svtv-data-obj->pipeline)
         (:pipeline-validp . svtv-data-obj->pipeline-validp))
       'change-svtv-data-obj
       'nil))