		Search-engine friendly clone of the ACL2 documentation.

Vl-lintresult

Change-vl-lintresult

Modifying constructor for vl-lintresult structures.

Syntax

(change-vl-lintresult x 
                      [:design <design>] 
                      [:design0 <design0>] 
                      [:design-orig <design-orig>] 
                      [:sv-modalist <sv-modalist>] 
                      [:reportcard <reportcard>] 
                      [:sd-probs <sd-probs>])

This is an often useful alternative to make-vl-lintresult.

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

(defmacro change-vl-lintresult (x &rest args)
  (std::change-aggregate
       'vl-lintresult
       x args
       '((:design . vl-lintresult->design)
         (:design0 . vl-lintresult->design0)
         (:design-orig . vl-lintresult->design-orig)
         (:sv-modalist . vl-lintresult->sv-modalist)
         (:reportcard . vl-lintresult->reportcard)
         (:sd-probs . vl-lintresult->sd-probs))
       'change-vl-lintresult
       'nil))