(vl-paramdecl-enumname-declarations x seen) → (mv new-x warnings paramdecls seen-out)
Function:
(defun vl-paramdecl-enumname-declarations (x seen) (declare (xargs :guard (and (vl-paramdecl-p x) (vl-datatype-map-p seen)))) (let ((__function__ 'vl-paramdecl-enumname-declarations)) (declare (ignorable __function__)) (b* (((vl-paramdecl x)) ((mv new-type warnings paramdecls seen) (vl-paramtype-case x.type :vl-typeparam (b* (((mv type warnings paramdecls seen) (if x.type.default (vl-datatype-enumname-declarations x.type.default nil x.loc seen) (mv nil nil nil (vl-datatype-map-fix seen))))) (mv (change-vl-typeparam x.type :default type) warnings paramdecls seen)) :vl-explicitvalueparam (b* (((mv type warnings paramdecls seen) (vl-datatype-enumname-declarations x.type.type nil x.loc seen))) (mv (change-vl-explicitvalueparam x.type :type type) warnings paramdecls seen)) :otherwise (mv x.type nil nil (vl-datatype-map-fix seen))))) (mv (change-vl-paramdecl x :type new-type) warnings paramdecls seen))))
Theorem:
(defthm vl-paramdecl-p-of-vl-paramdecl-enumname-declarations.new-x (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecl-enumname-declarations x seen))) (vl-paramdecl-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-paramdecl-enumname-declarations.warnings (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecl-enumname-declarations x seen))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-paramdecl-enumname-declarations.paramdecls (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecl-enumname-declarations x seen))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-map-p-of-vl-paramdecl-enumname-declarations.seen-out (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-paramdecl-enumname-declarations x seen))) (vl-datatype-map-p seen-out)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecl-enumname-declarations-of-vl-paramdecl-fix-x (equal (vl-paramdecl-enumname-declarations (vl-paramdecl-fix x) seen) (vl-paramdecl-enumname-declarations x seen)))
Theorem:
(defthm vl-paramdecl-enumname-declarations-vl-paramdecl-equiv-congruence-on-x (implies (vl-paramdecl-equiv x x-equiv) (equal (vl-paramdecl-enumname-declarations x seen) (vl-paramdecl-enumname-declarations x-equiv seen))) :rule-classes :congruence)
Theorem:
(defthm vl-paramdecl-enumname-declarations-of-vl-datatype-map-fix-seen (equal (vl-paramdecl-enumname-declarations x (vl-datatype-map-fix seen)) (vl-paramdecl-enumname-declarations x seen)))
Theorem:
(defthm vl-paramdecl-enumname-declarations-vl-datatype-map-equiv-congruence-on-seen (implies (vl-datatype-map-equiv seen seen-equiv) (equal (vl-paramdecl-enumname-declarations x seen) (vl-paramdecl-enumname-declarations x seen-equiv))) :rule-classes :congruence)