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