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