		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-package-scope-item-alist-top

Signature
(vl-package-scope-item-alist-top x) → *
Arguments: x — Guard (vl-package-p x).

The -aux function is memoized. In a single-threaded context, there would be no need to call make-fast-alist again. But for multi-threaded code, e.g., the vl-server, the alist may only be fast in some threads. Calling make-fast-alist again corrects for this and should be very cheap in the single-threaded case.

Definitions and Theorems

Function: vl-package-scope-item-alist-top

(defun vl-package-scope-item-alist-top (x)
 (declare (xargs :guard (vl-package-p x)))
 (let ((__function__ 'vl-package-scope-item-alist-top))
  (declare (ignorable __function__))
  (mbe
      :logic (vl-package-scope-item-alist x nil)
      :exec (make-fast-alist (vl-package-scope-item-alist-aux x)))))

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

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

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

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

Subtopics

Vl-package-scope-item-alist-aux: Memoized version.