Scopesubstitute into a vl-paramtype-p.
(vl-paramtype-scopesubst x ss) → new-x
Function:
(defun vl-paramtype-scopesubst (x ss) (declare (xargs :guard (and (vl-paramtype-p x) (vl-scopestack-p ss)))) (declare (ignorable x ss)) (let ((__function__ 'vl-paramtype-scopesubst)) (declare (ignorable __function__)) (vl-paramtype-case x (:vl-implicitvalueparam (change-vl-implicitvalueparam x :range (vl-maybe-range-scopesubst x.range ss) :default (vl-maybe-expr-scopesubst x.default ss))) (:vl-explicitvalueparam (change-vl-explicitvalueparam x :type (vl-datatype-scopesubst x.type ss) :default (vl-maybe-expr-scopesubst x.default ss))) (:vl-typeparam (change-vl-typeparam x :default (vl-maybe-datatype-scopesubst x.default ss))))))
Theorem:
(defthm vl-paramtype-p-of-vl-paramtype-scopesubst (b* ((new-x (vl-paramtype-scopesubst x ss))) (vl-paramtype-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramtype-scopesubst-of-vl-paramtype-fix-x (equal (vl-paramtype-scopesubst (vl-paramtype-fix x) ss) (vl-paramtype-scopesubst x ss)))
Theorem:
(defthm vl-paramtype-scopesubst-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-paramtype-scopesubst x ss) (vl-paramtype-scopesubst x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-paramtype-scopesubst-of-vl-scopestack-fix-ss (equal (vl-paramtype-scopesubst x (vl-scopestack-fix ss)) (vl-paramtype-scopesubst x ss)))
Theorem:
(defthm vl-paramtype-scopesubst-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-paramtype-scopesubst x ss) (vl-paramtype-scopesubst x ss-equiv))) :rule-classes :congruence)