(vl-configlist-gather-reportcard x acc) → new-acc
Function:
(defun vl-configlist-gather-reportcard (x acc) (declare (xargs :guard (and (vl-configlist-p x) (vl-reportcard-p acc)))) (let ((__function__ 'vl-configlist-gather-reportcard)) (declare (ignorable __function__)) (b* (((when (atom x)) (vl-reportcard-fix acc)) (acc (vl-extend-reportcard-list (vl-config->name (car x)) (vl-config->warnings (car x)) acc))) (vl-configlist-gather-reportcard (cdr x) acc))))
Theorem:
(defthm vl-reportcard-p-of-vl-configlist-gather-reportcard (b* ((new-acc (vl-configlist-gather-reportcard x acc))) (vl-reportcard-p new-acc)) :rule-classes :rewrite)
Theorem:
(defthm vl-configlist-gather-reportcard-of-vl-configlist-fix-x (equal (vl-configlist-gather-reportcard (vl-configlist-fix x) acc) (vl-configlist-gather-reportcard x acc)))
Theorem:
(defthm vl-configlist-gather-reportcard-vl-configlist-equiv-congruence-on-x (implies (vl-configlist-equiv x x-equiv) (equal (vl-configlist-gather-reportcard x acc) (vl-configlist-gather-reportcard x-equiv acc))) :rule-classes :congruence)
Theorem:
(defthm vl-configlist-gather-reportcard-of-vl-reportcard-fix-acc (equal (vl-configlist-gather-reportcard x (vl-reportcard-fix acc)) (vl-configlist-gather-reportcard x acc)))
Theorem:
(defthm vl-configlist-gather-reportcard-vl-reportcard-equiv-congruence-on-acc (implies (vl-reportcard-equiv acc acc-equiv) (equal (vl-configlist-gather-reportcard x acc) (vl-configlist-gather-reportcard x acc-equiv))) :rule-classes :congruence)