Look up a name in a (single) lexical scope.
(vl-lexscope-find name scope) → entry
Function:
(defun vl-lexscope-find (name scope) (declare (xargs :guard (and (stringp name) (vl-lexscope-p scope)))) (let ((__function__ 'vl-lexscope-find)) (declare (ignorable __function__)) (b* (((vl-lexscope scope)) (entry1 (cdr (hons-get (string-fix name) scope.decls))) (packages (vl-packagemap-find-packages-for-name name scope.wildpkgs)) ((when entry1) (if packages (change-vl-lexscope-entry entry1 :wildpkgs packages) entry1)) ((when packages) (make-vl-lexscope-entry :wildpkgs packages))) nil)))
Theorem:
(defthm return-type-of-vl-lexscope-find (b* ((entry (vl-lexscope-find name scope))) (iff (vl-lexscope-entry-p entry) entry)) :rule-classes :rewrite)
Theorem:
(defthm vl-lexscope-find-of-str-fix-name (equal (vl-lexscope-find (str-fix name) scope) (vl-lexscope-find name scope)))
Theorem:
(defthm vl-lexscope-find-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-lexscope-find name scope) (vl-lexscope-find name-equiv scope))) :rule-classes :congruence)
Theorem:
(defthm vl-lexscope-find-of-vl-lexscope-fix-scope (equal (vl-lexscope-find name (vl-lexscope-fix scope)) (vl-lexscope-find name scope)))
Theorem:
(defthm vl-lexscope-find-vl-lexscope-equiv-congruence-on-scope (implies (vl-lexscope-equiv scope scope-equiv) (equal (vl-lexscope-find name scope) (vl-lexscope-find name scope-equiv))) :rule-classes :congruence)