Add any warnings from a vl-reportcard-p to a vl-typedef-p.
(vl-typedef-apply-reportcard x reportcard) → new-x
Function:
(defun vl-typedef-apply-reportcard (x reportcard) (declare (xargs :guard (and (vl-typedef-p x) (vl-reportcard-p reportcard)))) (let ((__function__ 'vl-typedef-apply-reportcard)) (declare (ignorable __function__)) (b* (((vl-typedef x) x) (entry (hons-get x.name (vl-reportcard-fix reportcard))) ((unless entry) (vl-typedef-fix x))) (change-vl-typedef x :warnings (revappend-without-guard (cdr entry) x.warnings)))))
Theorem:
(defthm vl-typedef-p-of-vl-typedef-apply-reportcard (b* ((new-x (vl-typedef-apply-reportcard x reportcard))) (vl-typedef-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-typedef-apply-reportcard-of-vl-typedef-fix-x (equal (vl-typedef-apply-reportcard (vl-typedef-fix x) reportcard) (vl-typedef-apply-reportcard x reportcard)))
Theorem:
(defthm vl-typedef-apply-reportcard-vl-typedef-equiv-congruence-on-x (implies (vl-typedef-equiv x x-equiv) (equal (vl-typedef-apply-reportcard x reportcard) (vl-typedef-apply-reportcard x-equiv reportcard))) :rule-classes :congruence)
Theorem:
(defthm vl-typedef-apply-reportcard-of-vl-reportcard-fix-reportcard (equal (vl-typedef-apply-reportcard x (vl-reportcard-fix reportcard)) (vl-typedef-apply-reportcard x reportcard)))
Theorem:
(defthm vl-typedef-apply-reportcard-vl-reportcard-equiv-congruence-on-reportcard (implies (vl-reportcard-equiv reportcard reportcard-equiv) (equal (vl-typedef-apply-reportcard x reportcard) (vl-typedef-apply-reportcard x reportcard-equiv))) :rule-classes :congruence)