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