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