(vl-enumitemlist-enumname-declarations x lastval basetype atts loc) → (mv warnings paramdecls)
Function:
(defun vl-enumitemlist-enumname-declarations (x lastval basetype atts loc) (declare (xargs :guard (and (vl-enumitemlist-p x) (vl-expr-p lastval) (vl-datatype-p basetype) (vl-atts-p atts) (vl-location-p loc)))) (let ((__function__ 'vl-enumitemlist-enumname-declarations)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv warnings decls nextval) (vl-enumname-declarations (car x) lastval basetype atts loc)) ((mv warnings-rest decls-rest) (vl-enumitemlist-enumname-declarations (cdr x) nextval basetype atts loc))) (mv (append-without-guard warnings warnings-rest) (append-without-guard decls decls-rest)))))
Theorem:
(defthm vl-warninglist-p-of-vl-enumitemlist-enumname-declarations.warnings (b* (((mv ?warnings ?paramdecls) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-enumitemlist-enumname-declarations.paramdecls (b* (((mv ?warnings ?paramdecls) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-enumitemlist-enumname-declarations-of-vl-enumitemlist-fix-x (equal (vl-enumitemlist-enumname-declarations (vl-enumitemlist-fix x) lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc)))
Theorem:
(defthm vl-enumitemlist-enumname-declarations-vl-enumitemlist-equiv-congruence-on-x (implies (vl-enumitemlist-equiv x x-equiv) (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x-equiv lastval basetype atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-enumitemlist-enumname-declarations-of-vl-expr-fix-lastval (equal (vl-enumitemlist-enumname-declarations x (vl-expr-fix lastval) basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc)))
Theorem:
(defthm vl-enumitemlist-enumname-declarations-vl-expr-equiv-congruence-on-lastval (implies (vl-expr-equiv lastval lastval-equiv) (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval-equiv basetype atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-enumitemlist-enumname-declarations-of-vl-datatype-fix-basetype (equal (vl-enumitemlist-enumname-declarations x lastval (vl-datatype-fix basetype) atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc)))
Theorem:
(defthm vl-enumitemlist-enumname-declarations-vl-datatype-equiv-congruence-on-basetype (implies (vl-datatype-equiv basetype basetype-equiv) (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype-equiv atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-enumitemlist-enumname-declarations-of-vl-atts-fix-atts (equal (vl-enumitemlist-enumname-declarations x lastval basetype (vl-atts-fix atts) loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc)))
Theorem:
(defthm vl-enumitemlist-enumname-declarations-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-enumitemlist-enumname-declarations-of-vl-location-fix-loc (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts (vl-location-fix loc)) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc)))
Theorem:
(defthm vl-enumitemlist-enumname-declarations-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-enumitemlist-enumname-declarations x lastval basetype atts loc) (vl-enumitemlist-enumname-declarations x lastval basetype atts loc-equiv))) :rule-classes :congruence)