(vl-shadowcheck-push-scope x st) → st
Function:
(defun vl-shadowcheck-push-scope (x st) (declare (xargs :guard (and (vl-scope-p x) (vl-shadowcheck-state-p st)))) (let ((__function__ 'vl-shadowcheck-push-scope)) (declare (ignorable __function__)) (b* (((vl-shadowcheck-state st))) (change-vl-shadowcheck-state st :lexscopes (vl-lexscopes-enter-new-scope st.lexscopes) :ss (vl-scopestack-push x st.ss)))))
Theorem:
(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-push-scope (b* ((st (vl-shadowcheck-push-scope x st))) (vl-shadowcheck-state-p st)) :rule-classes :rewrite)
Theorem:
(defthm vl-shadowcheck-push-scope-of-vl-scope-fix-x (equal (vl-shadowcheck-push-scope (vl-scope-fix x) st) (vl-shadowcheck-push-scope x st)))
Theorem:
(defthm vl-shadowcheck-push-scope-vl-scope-equiv-congruence-on-x (implies (vl-scope-equiv x x-equiv) (equal (vl-shadowcheck-push-scope x st) (vl-shadowcheck-push-scope x-equiv st))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-push-scope-of-vl-shadowcheck-state-fix-st (equal (vl-shadowcheck-push-scope x (vl-shadowcheck-state-fix st)) (vl-shadowcheck-push-scope x st)))
Theorem:
(defthm vl-shadowcheck-push-scope-vl-shadowcheck-state-equiv-congruence-on-st (implies (vl-shadowcheck-state-equiv st st-equiv) (equal (vl-shadowcheck-push-scope x st) (vl-shadowcheck-push-scope x st-equiv))) :rule-classes :congruence)