Scopesubstitute into a vl-enumbasetype-p.
(vl-enumbasetype-scopesubst x ss) → new-x
Function:
(defun vl-enumbasetype-scopesubst (x ss) (declare (xargs :guard (and (vl-enumbasetype-p x) (vl-scopestack-p ss)))) (declare (ignorable x ss)) (let ((__function__ 'vl-enumbasetype-scopesubst)) (declare (ignorable __function__)) (b* (((vl-enumbasetype x) x)) (change-vl-enumbasetype x :dim (vl-maybe-packeddimension-scopesubst x.dim ss)))))
Theorem:
(defthm vl-enumbasetype-p-of-vl-enumbasetype-scopesubst (b* ((new-x (vl-enumbasetype-scopesubst x ss))) (vl-enumbasetype-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-enumbasetype-scopesubst-of-vl-enumbasetype-fix-x (equal (vl-enumbasetype-scopesubst (vl-enumbasetype-fix x) ss) (vl-enumbasetype-scopesubst x ss)))
Theorem:
(defthm vl-enumbasetype-scopesubst-vl-enumbasetype-equiv-congruence-on-x (implies (vl-enumbasetype-equiv x x-equiv) (equal (vl-enumbasetype-scopesubst x ss) (vl-enumbasetype-scopesubst x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-enumbasetype-scopesubst-of-vl-scopestack-fix-ss (equal (vl-enumbasetype-scopesubst x (vl-scopestack-fix ss)) (vl-enumbasetype-scopesubst x ss)))
Theorem:
(defthm vl-enumbasetype-scopesubst-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-enumbasetype-scopesubst x ss) (vl-enumbasetype-scopesubst x ss-equiv))) :rule-classes :congruence)