(vl-typedef-enumname-declarations x seen) → (mv new-x warnings paramdecls seen-out)
Function:
(defun vl-typedef-enumname-declarations (x seen) (declare (xargs :guard (and (vl-typedef-p x) (vl-datatype-map-p seen)))) (let ((__function__ 'vl-typedef-enumname-declarations)) (declare (ignorable __function__)) (b* (((vl-typedef x)) ((mv new-type warnings paramdecls seen) (vl-datatype-enumname-declarations x.type x.name x.minloc seen))) (mv (change-vl-typedef x :type new-type) warnings paramdecls seen))))
Theorem:
(defthm vl-typedef-p-of-vl-typedef-enumname-declarations.new-x (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-typedef-enumname-declarations x seen))) (vl-typedef-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-typedef-enumname-declarations.warnings (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-typedef-enumname-declarations x seen))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-typedef-enumname-declarations.paramdecls (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-typedef-enumname-declarations x seen))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-map-p-of-vl-typedef-enumname-declarations.seen-out (b* (((mv ?new-x ?warnings ?paramdecls ?seen-out) (vl-typedef-enumname-declarations x seen))) (vl-datatype-map-p seen-out)) :rule-classes :rewrite)
Theorem:
(defthm vl-typedef-enumname-declarations-of-vl-typedef-fix-x (equal (vl-typedef-enumname-declarations (vl-typedef-fix x) seen) (vl-typedef-enumname-declarations x seen)))
Theorem:
(defthm vl-typedef-enumname-declarations-vl-typedef-equiv-congruence-on-x (implies (vl-typedef-equiv x x-equiv) (equal (vl-typedef-enumname-declarations x seen) (vl-typedef-enumname-declarations x-equiv seen))) :rule-classes :congruence)
Theorem:
(defthm vl-typedef-enumname-declarations-of-vl-datatype-map-fix-seen (equal (vl-typedef-enumname-declarations x (vl-datatype-map-fix seen)) (vl-typedef-enumname-declarations x seen)))
Theorem:
(defthm vl-typedef-enumname-declarations-vl-datatype-map-equiv-congruence-on-seen (implies (vl-datatype-map-equiv seen seen-equiv) (equal (vl-typedef-enumname-declarations x seen) (vl-typedef-enumname-declarations x seen-equiv))) :rule-classes :congruence)