		Search-engine friendly clone of the ACL2 documentation.

Vl-iframe

Make-vl-iframe

Basic constructor macro for vl-iframe structures.

Syntax

(make-vl-iframe [: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 the usual way to construct vl-iframe structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-iframe structure from scratch. See also change-vl-iframe, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-iframe

(defmacro make-vl-iframe (&rest args)
  (std::make-aggregate 'vl-iframe
                       args
                       '((:initially-activep)
                         (:some-thing-satisfiedp)
                         (:already-saw-elsep)
                         (:mi-controller)
                         (:mi-filename))
                       'make-vl-iframe
                       nil))

Function: vl-iframe

(defun vl-iframe
       (initially-activep some-thing-satisfiedp already-saw-elsep
                          mi-controller mi-filename)
 (declare (xargs :guard (and (booleanp initially-activep)
                             (booleanp some-thing-satisfiedp)
                             (booleanp already-saw-elsep)
                             (maybe-stringp mi-controller)
                             (maybe-stringp mi-filename))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-iframe))
  (declare (ignorable __function__))
  (b* ((initially-activep
            (mbe :logic (acl2::bool-fix initially-activep)
                 :exec initially-activep))
       (some-thing-satisfiedp
            (mbe :logic (acl2::bool-fix some-thing-satisfiedp)
                 :exec some-thing-satisfiedp))
       (already-saw-elsep
            (mbe :logic (acl2::bool-fix already-saw-elsep)
                 :exec already-saw-elsep))
       (mi-controller (mbe :logic (maybe-string-fix mi-controller)
                           :exec mi-controller))
       (mi-filename (mbe :logic (maybe-string-fix mi-filename)
                         :exec mi-filename)))
   (std::prod-cons
     (std::prod-cons initially-activep some-thing-satisfiedp)
     (std::prod-cons already-saw-elsep
                     (std::prod-cons mi-controller mi-filename))))))