Push a new scope onto the lexical scope stack.
(vl-lexscopes-enter-new-scope scopes) → scopes
This should be called when entering a module, function, block, etc.
Function:
(defun vl-lexscopes-enter-new-scope$inline (scopes) (declare (xargs :guard (vl-lexscopes-p scopes))) (let ((__function__ 'vl-lexscopes-enter-new-scope)) (declare (ignorable __function__)) (cons (vl-empty-lexscope) (vl-lexscopes-fix scopes))))
Theorem:
(defthm vl-lexscopes-p-of-vl-lexscopes-enter-new-scope (b* ((scopes (vl-lexscopes-enter-new-scope$inline scopes))) (vl-lexscopes-p scopes)) :rule-classes :rewrite)
Theorem:
(defthm vl-lexscopes-enter-new-scope$inline-of-vl-lexscopes-fix-scopes (equal (vl-lexscopes-enter-new-scope$inline (vl-lexscopes-fix scopes)) (vl-lexscopes-enter-new-scope$inline scopes)))
Theorem:
(defthm vl-lexscopes-enter-new-scope$inline-vl-lexscopes-equiv-congruence-on-scopes (implies (vl-lexscopes-equiv scopes scopes-equiv) (equal (vl-lexscopes-enter-new-scope$inline scopes) (vl-lexscopes-enter-new-scope$inline scopes-equiv))) :rule-classes :congruence)