Collect all types of warnings found in a reportcard.
(vl-reportcard-types x) → types
Function:
(defun vl-reportcard-types (x) (declare (xargs :guard (vl-reportcard-p x))) (let ((__function__ 'vl-reportcard-types)) (declare (ignorable __function__)) (b* ((x (vl-reportcard-fix x)) ((when (atom x)) nil)) (append (vl-warninglist->types (cdar x)) (vl-reportcard-types (cdr x))))))
Theorem:
(defthm symbol-listp-of-vl-reportcard-types (b* ((types (vl-reportcard-types x))) (symbol-listp types)) :rule-classes :rewrite)
Theorem:
(defthm vl-reportcard-types-of-vl-reportcard-fix-x (equal (vl-reportcard-types (vl-reportcard-fix x)) (vl-reportcard-types x)))
Theorem:
(defthm vl-reportcard-types-vl-reportcard-equiv-congruence-on-x (implies (vl-reportcard-equiv x x-equiv) (equal (vl-reportcard-types x) (vl-reportcard-types x-equiv))) :rule-classes :congruence)