		Search-engine friendly clone of the ACL2 documentation.

Vl-iframe

Change-vl-iframe

Modifying constructor for vl-iframe structures.

Syntax

(change-vl-iframe x 
                  [:initially-activep <initially-activep>] 
                  [:some-thing-satisfiedp <some-thing-satisfiedp>] 
                  [:already-saw-elsep <already-saw-elsep>] 
                  [:mi-controller <mi-controller>] 
                  [:mi-filename <mi-filename>])

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

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

(defmacro change-vl-iframe (x &rest args)
  (std::change-aggregate
       'vl-iframe
       x args
       '((:initially-activep . vl-iframe->initially-activep)
         (:some-thing-satisfiedp . vl-iframe->some-thing-satisfiedp)
         (:already-saw-elsep . vl-iframe->already-saw-elsep)
         (:mi-controller . vl-iframe->mi-controller)
         (:mi-filename . vl-iframe->mi-filename))
       'change-vl-iframe
       'remake-vl-iframe))