		Search-engine friendly clone of the ACL2 documentation.

Vl-package-scope-find-item

Vl-package-scope-item-alist

Signature
(vl-package-scope-item-alist scope acc) → alist
Arguments: scope — Guard (vl-package-p scope).
Returns: alist — Type (implies (vl-scopeitem-alist-p acc) (vl-scopeitem-alist-p alist)).

Definitions and Theorems

Function: vl-package-scope-item-alist

(defun vl-package-scope-item-alist (scope acc)
  (declare (xargs :guard (vl-package-p scope)))
  (let ((__function__ 'vl-package-scope-item-alist))
    (declare (ignorable __function__))
    (b* (((vl-package scope))
         (acc (vl-dpiimportlist-alist scope.dpiimports acc))
         (acc (vl-typedeflist-alist scope.typedefs acc))
         (acc (vl-taskdecllist-alist scope.taskdecls acc))
         (acc (vl-fundecllist-alist scope.fundecls acc))
         (acc (vl-vardecllist-alist scope.vardecls acc))
         (acc (vl-paramdecllist-alist scope.paramdecls acc)))
      acc)))

Theorem: return-type-of-vl-package-scope-item-alist

(defthm return-type-of-vl-package-scope-item-alist
  (b* ((alist (vl-package-scope-item-alist scope acc)))
    (implies (vl-scopeitem-alist-p acc)
             (vl-scopeitem-alist-p alist)))
  :rule-classes :rewrite)

Theorem: vl-package-scope-item-alist-lookup-acc-elim

(defthm vl-package-scope-item-alist-lookup-acc-elim
 (implies
  (syntaxp (not (equal acc ''nil)))
  (equal
      (hons-assoc-equal name
                        (vl-package-scope-item-alist scope acc))
      (or (hons-assoc-equal name
                            (vl-package-scope-item-alist scope nil))
          (hons-assoc-equal name acc)))))

Theorem: vl-package-scope-item-alist-correct

(defthm vl-package-scope-item-alist-correct
 (implies
   (stringp name)
   (equal (hons-assoc-equal name
                            (vl-package-scope-item-alist scope nil))
          (b* ((item (vl-package-scope-find-item name scope)))
            (and item (cons name item))))))

Theorem: vl-package-scope-item-alist-of-vl-package-fix-scope

(defthm vl-package-scope-item-alist-of-vl-package-fix-scope
  (equal (vl-package-scope-item-alist (vl-package-fix scope)
                                      acc)
         (vl-package-scope-item-alist scope acc)))

Theorem: vl-package-scope-item-alist-vl-package-equiv-congruence-on-scope

(defthm
   vl-package-scope-item-alist-vl-package-equiv-congruence-on-scope
  (implies (vl-package-equiv scope scope-equiv)
           (equal (vl-package-scope-item-alist scope acc)
                  (vl-package-scope-item-alist scope-equiv acc)))
  :rule-classes :congruence)