		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-design-scope-package-alist-top

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

Definitions and Theorems

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

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

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

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

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

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

Subtopics

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