		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>])

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))
                       'make-vl-lexscope-entry
                       nil))

Function: vl-lexscope-entry

(defun vl-lexscope-entry (decl direct-pkg wildpkgs)
 (declare (xargs :guard (and (acl2::any-p decl)
                             (maybe-stringp direct-pkg)
                             (string-listp wildpkgs))))
 (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)))
     (cons :vl-lexscope-entry
           (std::prod-cons decl
                           (std::prod-cons direct-pkg wildpkgs))))))