Memoized core.
(vl-scope-package-alist-aux scope) → alist
Function:
(defun vl-scope-package-alist-aux (scope) (declare (xargs :guard (vl-scope-p scope))) (let ((__function__ 'vl-scope-package-alist-aux)) (declare (ignorable __function__)) (b* ((scope (vl-scope-fix scope))) (case (tag scope) (:vl-design (b* (((vl-design scope :quietp t))) (make-fast-alist (vl-design-scope-package-alist scope nil)))) (otherwise nil)))))
Theorem:
(defthm vl-package-alist-p-of-vl-scope-package-alist-aux (b* ((alist (vl-scope-package-alist-aux scope))) (vl-package-alist-p alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-scope-package-alist-aux-correct (implies (stringp name) (equal (cdr (hons-assoc-equal name (vl-scope-package-alist-aux scope))) (vl-scope-find-package name scope))))
Theorem:
(defthm vl-scope-package-alist-aux-of-vl-scope-fix-scope (equal (vl-scope-package-alist-aux (vl-scope-fix scope)) (vl-scope-package-alist-aux scope)))
Theorem:
(defthm vl-scope-package-alist-aux-vl-scope-equiv-congruence-on-scope (implies (vl-scope-equiv scope scope-equiv) (equal (vl-scope-package-alist-aux scope) (vl-scope-package-alist-aux scope-equiv))) :rule-classes :congruence)