		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscopes

Vl-lexscopes-exit-scope

Pop the current scope off of the lexical scope stack and free fast alists.

Signature
(vl-lexscopes-exit-scope scopes) → scopes
Arguments: scopes — Guard (vl-lexscopes-p scopes).
Returns: scopes — Type (vl-lexscopes-p scopes).

This should be called when exiting a module, function, block, etc.

Definitions and Theorems

Function: vl-lexscopes-exit-scope

(defun vl-lexscopes-exit-scope (scopes)
  (declare (xargs :guard (vl-lexscopes-p scopes)))
  (let ((__function__ 'vl-lexscopes-exit-scope))
    (declare (ignorable __function__))
    (b* ((scopes (vl-lexscopes-fix scopes))
         ((when (atom scopes))
          (raise "Expected at least one lexscope."))
         ((cons head tail) scopes))
      (fast-alist-free head)
      tail)))

Theorem: vl-lexscopes-p-of-vl-lexscopes-exit-scope

(defthm vl-lexscopes-p-of-vl-lexscopes-exit-scope
  (b* ((scopes (vl-lexscopes-exit-scope scopes)))
    (vl-lexscopes-p scopes))
  :rule-classes :rewrite)

Theorem: vl-lexscopes-exit-scope-of-vl-lexscopes-fix-scopes

(defthm vl-lexscopes-exit-scope-of-vl-lexscopes-fix-scopes
  (equal (vl-lexscopes-exit-scope (vl-lexscopes-fix scopes))
         (vl-lexscopes-exit-scope scopes)))

Theorem: vl-lexscopes-exit-scope-vl-lexscopes-equiv-congruence-on-scopes

(defthm
    vl-lexscopes-exit-scope-vl-lexscopes-equiv-congruence-on-scopes
  (implies (vl-lexscopes-equiv scopes scopes-equiv)
           (equal (vl-lexscopes-exit-scope scopes)
                  (vl-lexscopes-exit-scope scopes-equiv)))
  :rule-classes :congruence)