		Search-engine friendly clone of the ACL2 documentation.

Vl-importresult

Make-vl-importresult

Basic constructor macro for vl-importresult structures.

Syntax

(make-vl-importresult [:item <item>] 
                      [:pkg-name <pkg-name>] 
                      [:loc <loc>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-importresult

(defmacro make-vl-importresult (&rest args)
  (std::make-aggregate 'vl-importresult
                       args '((:item) (:pkg-name) (:loc))
                       'make-vl-importresult
                       nil))

Function: vl-importresult

(defun vl-importresult (item pkg-name loc)
  (declare (xargs :guard (and (vl-maybe-scopeitem-p item)
                              (stringp pkg-name)
                              (vl-location-p loc))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-importresult))
    (declare (ignorable __function__))
    (b* ((item (mbe :logic (vl-maybe-scopeitem-fix item)
                    :exec item))
         (pkg-name (mbe :logic (str-fix pkg-name)
                        :exec pkg-name))
         (loc (mbe :logic (vl-location-fix loc)
                   :exec loc)))
      (cons :vl-importresult
            (std::prod-cons item (std::prod-cons pkg-name loc))))))