		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscope

Vl-lexscope-find

Look up a name in a lexical scope.

Signature
(vl-lexscope-find name scope) → entry
Arguments: name — Guard (stringp name).; scope — Guard (vl-lexscope-p scope).
Returns: entry — Type (iff (vl-lexscope-entry-p entry) entry).

Definitions and Theorems

Function: vl-lexscope-find$inline

(defun vl-lexscope-find$inline (name scope)
  (declare (xargs :guard (and (stringp name)
                              (vl-lexscope-p scope))))
  (let ((__function__ 'vl-lexscope-find))
    (declare (ignorable __function__))
    (cdr (hons-get (string-fix name)
                   (vl-lexscope-fix scope)))))

Theorem: return-type-of-vl-lexscope-find

(defthm return-type-of-vl-lexscope-find
  (b* ((entry (vl-lexscope-find$inline name scope)))
    (iff (vl-lexscope-entry-p entry) entry))
  :rule-classes :rewrite)

Theorem: vl-lexscope-find$inline-of-str-fix-name

(defthm vl-lexscope-find$inline-of-str-fix-name
  (equal (vl-lexscope-find$inline (str-fix name)
                                  scope)
         (vl-lexscope-find$inline name scope)))

Theorem: vl-lexscope-find$inline-streqv-congruence-on-name

(defthm vl-lexscope-find$inline-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-lexscope-find$inline name scope)
                  (vl-lexscope-find$inline name-equiv scope)))
  :rule-classes :congruence)

Theorem: vl-lexscope-find$inline-of-vl-lexscope-fix-scope

(defthm vl-lexscope-find$inline-of-vl-lexscope-fix-scope
  (equal (vl-lexscope-find$inline name (vl-lexscope-fix scope))
         (vl-lexscope-find$inline name scope)))

Theorem: vl-lexscope-find$inline-vl-lexscope-equiv-congruence-on-scope

(defthm
      vl-lexscope-find$inline-vl-lexscope-equiv-congruence-on-scope
  (implies (vl-lexscope-equiv scope scope-equiv)
           (equal (vl-lexscope-find$inline name scope)
                  (vl-lexscope-find$inline name scope-equiv)))
  :rule-classes :congruence)