		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scope-definition-alist

Make a fast lookup table for definitions in a scope. Memoized.

Signature
(vl-scope-definition-alist scope) → alist
Arguments: scope — Guard (vl-scope-p scope).
Returns: alist — Type (vl-scopedef-alist-p alist).

Definitions and Theorems

Function: vl-scope-definition-alist

(defun
     vl-scope-definition-alist (scope)
     (declare (xargs :guard (vl-scope-p scope)))
     (let ((__function__ 'vl-scope-definition-alist))
          (declare (ignorable __function__))
          (make-fast-alist (vl-scope-definition-alist-aux scope))))

Theorem: vl-scopedef-alist-p-of-vl-scope-definition-alist

(defthm vl-scopedef-alist-p-of-vl-scope-definition-alist
        (b* ((alist (vl-scope-definition-alist scope)))
            (vl-scopedef-alist-p alist))
        :rule-classes :rewrite)

Theorem: vl-scope-definition-alist-correct

(defthm
 vl-scope-definition-alist-correct
 (implies
  (stringp name)
  (equal
     (cdr (hons-assoc-equal name (vl-scope-definition-alist scope)))
     (vl-scope-find-definition name scope))))

Theorem: vl-scope-definition-alist-of-vl-scope-fix-scope

(defthm vl-scope-definition-alist-of-vl-scope-fix-scope
        (equal (vl-scope-definition-alist (vl-scope-fix scope))
               (vl-scope-definition-alist scope)))

Theorem: vl-scope-definition-alist-vl-scope-equiv-congruence-on-scope

(defthm vl-scope-definition-alist-vl-scope-equiv-congruence-on-scope
        (implies (vl-scope-equiv scope scope-equiv)
                 (equal (vl-scope-definition-alist scope)
                        (vl-scope-definition-alist scope-equiv)))
        :rule-classes :congruence)

Subtopics

Vl-scope-definition-alist-aux: Memoized core.