(vl-shadowcheck-paramtype x ctx st warnings) → (mv st warnings)
Function:
(defun vl-shadowcheck-paramtype (x ctx st warnings) (declare (xargs :guard (and (vl-paramtype-p x) (any-p ctx) (vl-shadowcheck-state-p st) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-shadowcheck-paramtype)) (declare (ignorable __function__)) (vl-paramtype-case x :vl-implicitvalueparam (b* (((mv st warnings) (vl-shadowcheck-maybe-range x.range ctx st warnings)) ((mv st warnings) (vl-shadowcheck-maybe-expr x.default ctx st warnings))) (mv st warnings)) :vl-explicitvalueparam (b* (((mv st warnings) (vl-shadowcheck-datatype x.type ctx st warnings)) ((mv st warnings) (vl-shadowcheck-maybe-expr x.default ctx st warnings))) (mv st warnings)) :vl-typeparam (vl-shadowcheck-maybe-datatype x.default ctx st warnings))))
Theorem:
(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-paramtype.st (b* (((mv ?st ?warnings) (vl-shadowcheck-paramtype x ctx st warnings))) (vl-shadowcheck-state-p st)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-shadowcheck-paramtype.warnings (b* (((mv ?st ?warnings) (vl-shadowcheck-paramtype x ctx st warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-shadowcheck-paramtype-of-vl-paramtype-fix-x (equal (vl-shadowcheck-paramtype (vl-paramtype-fix x) ctx st warnings) (vl-shadowcheck-paramtype x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-paramtype-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-shadowcheck-paramtype x ctx st warnings) (vl-shadowcheck-paramtype x-equiv ctx st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-paramtype-of-identity-ctx (equal (vl-shadowcheck-paramtype x (identity ctx) st warnings) (vl-shadowcheck-paramtype x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-paramtype-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-shadowcheck-paramtype x ctx st warnings) (vl-shadowcheck-paramtype x ctx-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-paramtype-of-vl-shadowcheck-state-fix-st (equal (vl-shadowcheck-paramtype x ctx (vl-shadowcheck-state-fix st) warnings) (vl-shadowcheck-paramtype x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-paramtype-vl-shadowcheck-state-equiv-congruence-on-st (implies (vl-shadowcheck-state-equiv st st-equiv) (equal (vl-shadowcheck-paramtype x ctx st warnings) (vl-shadowcheck-paramtype x ctx st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-paramtype-of-vl-warninglist-fix-warnings (equal (vl-shadowcheck-paramtype x ctx st (vl-warninglist-fix warnings)) (vl-shadowcheck-paramtype x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-paramtype-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-shadowcheck-paramtype x ctx st warnings) (vl-shadowcheck-paramtype x ctx st warnings-equiv))) :rule-classes :congruence)