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