		Search-engine friendly clone of the ACL2 documentation.

Vl-immdepgraph

Change-vl-immdepgraph

Modifying constructor for vl-immdepgraph structures.

Syntax

(change-vl-immdepgraph x 
                       [:all-okp <all-okp>] 
                       [:deps <deps>] 
                       [:reportcard <reportcard>])

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

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

(defmacro change-vl-immdepgraph (x &rest args)
  (std::change-aggregate
       'vl-immdepgraph
       x args
       '((:all-okp . vl-immdepgraph->all-okp)
         (:deps . vl-immdepgraph->deps)
         (:reportcard . vl-immdepgraph->reportcard))
       'change-vl-immdepgraph
       'remake-vl-immdepgraph))