		Search-engine friendly clone of the ACL2 documentation.

Defsvtv-args

Change-defsvtv-args

Modifying constructor for defsvtv-args structures.

Syntax

(change-defsvtv-args x 
                     [:name <name>] 
                     [:stages <stages>] 
                     [:inputs <inputs>] 
                     [:overrides <overrides>] 
                     [:outputs <outputs>] 
                     [:internals <internals>] 
                     [:design <design>] 
                     [:design-const <design-const>] 
                     [:labels <labels>] 
                     [:phase-config <phase-config>] 
                     [:clocks <clocks>] 
                     [:phase-scc-limit <phase-scc-limit>] 
                     [:monotonify <monotonify>] 
                     [:simplify <simplify>] 
                     [:pre-simplify <pre-simplify>] 
                     [:pipe-simp <pipe-simp>] 
                     [:cycle-phases <cycle-phases>] 
                     [:cycle-phases-p <cycle-phases-p>] 
                     [:cycle-simp <cycle-simp>] 
                     [:initial-state-vars <initial-state-vars>] 
                     [:define-macros <define-macros>] 
                     [:define-mod <define-mod>] 
                     [:parents <parents>] 
                     [:short <short>] 
                     [:long <long>] 
                     [:form <form>])

This is an often useful alternative to make-defsvtv-args.

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

(defmacro change-defsvtv-args (x &rest args)
  (std::change-aggregate
       'defsvtv-args
       x args
       '((:name . defsvtv-args->name)
         (:stages . defsvtv-args->stages)
         (:inputs . defsvtv-args->inputs)
         (:overrides . defsvtv-args->overrides)
         (:outputs . defsvtv-args->outputs)
         (:internals . defsvtv-args->internals)
         (:design . defsvtv-args->design)
         (:design-const . defsvtv-args->design-const)
         (:labels . defsvtv-args->labels)
         (:phase-config . defsvtv-args->phase-config)
         (:clocks . defsvtv-args->clocks)
         (:phase-scc-limit . defsvtv-args->phase-scc-limit)
         (:monotonify . defsvtv-args->monotonify)
         (:simplify . defsvtv-args->simplify)
         (:pre-simplify . defsvtv-args->pre-simplify)
         (:pipe-simp . defsvtv-args->pipe-simp)
         (:cycle-phases . defsvtv-args->cycle-phases)
         (:cycle-phases-p . defsvtv-args->cycle-phases-p)
         (:cycle-simp . defsvtv-args->cycle-simp)
         (:initial-state-vars . defsvtv-args->initial-state-vars)
         (:define-macros . defsvtv-args->define-macros)
         (:define-mod . defsvtv-args->define-mod)
         (:parents . defsvtv-args->parents)
         (:short . defsvtv-args->short)
         (:long . defsvtv-args->long)
         (:form . defsvtv-args->form))
       'change-defsvtv-args
       'nil))