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