Add a list of warnings to a vl-reportcard-p.
(vl-extend-reportcard-list name warnings reportcard) → new-reportcard
We add all the warnings at once, i.e., with a single fast-alist update.
Function:
(defun vl-extend-reportcard-list (name warnings reportcard) (declare (xargs :guard (and (vl-reportcardkey-p name) (vl-warninglist-p warnings) (vl-reportcard-p reportcard)))) (let ((__function__ 'vl-extend-reportcard-list)) (declare (ignorable __function__)) (b* (((when (atom warnings)) (vl-reportcard-fix reportcard)) (name (vl-reportcardkey-fix name)) (warnings (vl-warninglist-fix warnings)) (reportcard (vl-reportcard-fix reportcard)) (old-warnings (cdr (hons-get name reportcard))) (new-warnings (append-without-guard warnings old-warnings))) (hons-acons name new-warnings reportcard))))
Theorem:
(defthm vl-reportcard-p-of-vl-extend-reportcard-list (b* ((new-reportcard (vl-extend-reportcard-list name warnings reportcard))) (vl-reportcard-p new-reportcard)) :rule-classes :rewrite)
Theorem:
(defthm vl-extend-reportcard-list-of-vl-reportcardkey-fix-name (equal (vl-extend-reportcard-list (vl-reportcardkey-fix name) warnings reportcard) (vl-extend-reportcard-list name warnings reportcard)))
Theorem:
(defthm vl-extend-reportcard-list-vl-reportcardkey-equiv-congruence-on-name (implies (vl-reportcardkey-equiv name name-equiv) (equal (vl-extend-reportcard-list name warnings reportcard) (vl-extend-reportcard-list name-equiv warnings reportcard))) :rule-classes :congruence)
Theorem:
(defthm vl-extend-reportcard-list-of-vl-warninglist-fix-warnings (equal (vl-extend-reportcard-list name (vl-warninglist-fix warnings) reportcard) (vl-extend-reportcard-list name warnings reportcard)))
Theorem:
(defthm vl-extend-reportcard-list-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-extend-reportcard-list name warnings reportcard) (vl-extend-reportcard-list name warnings-equiv reportcard))) :rule-classes :congruence)
Theorem:
(defthm vl-extend-reportcard-list-of-vl-reportcard-fix-reportcard (equal (vl-extend-reportcard-list name warnings (vl-reportcard-fix reportcard)) (vl-extend-reportcard-list name warnings reportcard)))
Theorem:
(defthm vl-extend-reportcard-list-vl-reportcard-equiv-congruence-on-reportcard (implies (vl-reportcard-equiv reportcard reportcard-equiv) (equal (vl-extend-reportcard-list name warnings reportcard) (vl-extend-reportcard-list name warnings reportcard-equiv))) :rule-classes :congruence)