(vl-module-scope-item-alist scope acc) → alist
Function:
(defun vl-module-scope-item-alist (scope acc) (declare (xargs :guard (vl-module-p scope))) (let ((__function__ 'vl-module-scope-item-alist)) (declare (ignorable __function__)) (b* (((vl-module scope)) (acc (vl-interfaceportlist-alist scope.ifports acc)) (acc (vl-genelementlist-alist scope.generates acc)) (acc (vl-genvarlist-alist scope.genvars acc)) (acc (vl-gateinstlist-alist scope.gateinsts acc)) (acc (vl-modinstlist-alist scope.modinsts acc)) (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:
(defthm return-type-of-vl-module-scope-item-alist (b* ((alist (vl-module-scope-item-alist scope acc))) (implies (vl-scopeitem-alist-p acc) (vl-scopeitem-alist-p alist))) :rule-classes :rewrite)
Theorem:
(defthm vl-module-scope-item-alist-lookup-acc-elim (implies (syntaxp (not (equal acc ''nil))) (equal (hons-assoc-equal name (vl-module-scope-item-alist scope acc)) (or (hons-assoc-equal name (vl-module-scope-item-alist scope nil)) (hons-assoc-equal name acc)))))
Theorem:
(defthm vl-module-scope-item-alist-correct (implies (stringp name) (equal (hons-assoc-equal name (vl-module-scope-item-alist scope nil)) (b* ((item (vl-module-scope-find-item name scope))) (and item (cons name item))))))
Theorem:
(defthm vl-module-scope-item-alist-of-vl-module-fix-scope (equal (vl-module-scope-item-alist (vl-module-fix scope) acc) (vl-module-scope-item-alist scope acc)))
Theorem:
(defthm vl-module-scope-item-alist-vl-module-equiv-congruence-on-scope (implies (vl-module-equiv scope scope-equiv) (equal (vl-module-scope-item-alist scope acc) (vl-module-scope-item-alist scope-equiv acc))) :rule-classes :congruence)