		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscope-entry

Make-vl-lexscope-entry

Basic constructor macro for vl-lexscope-entry structures.

Syntax

(make-vl-lexscope-entry [:decl <decl>] 
                        [:direct-pkg <direct-pkg>] 
                        [:wildpkgs <wildpkgs>] 
                        [:genblockp <genblockp>])

This is the usual way to construct vl-lexscope-entry structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-lexscope-entry

(defmacro make-vl-lexscope-entry (&rest args)
  (std::make-aggregate 'vl-lexscope-entry
                       args
                       '((:decl)
                         (:direct-pkg)
                         (:wildpkgs)
                         (:genblockp))
                       'make-vl-lexscope-entry
                       nil))

Function: vl-lexscope-entry

(defun vl-lexscope-entry (decl direct-pkg wildpkgs genblockp)
  (declare (xargs :guard (and (any-p decl)
                              (maybe-stringp direct-pkg)
                              (string-listp wildpkgs)
                              (booleanp genblockp))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-lexscope-entry))
    (declare (ignorable __function__))
    (b* ((decl (mbe :logic (identity decl) :exec decl))
         (direct-pkg (mbe :logic (maybe-string-fix direct-pkg)
                          :exec direct-pkg))
         (wildpkgs (mbe :logic (string-list-fix wildpkgs)
                        :exec wildpkgs))
         (genblockp (mbe :logic (acl2::bool-fix genblockp)
                         :exec genblockp)))
      (cons :vl-lexscope-entry
            (std::prod-cons (std::prod-cons decl direct-pkg)
                            (std::prod-cons wildpkgs genblockp))))))