		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard

Vl-reportcard-types

Collect all types of warnings found in a reportcard.

Signature
(vl-reportcard-types x) → types
Arguments: x — Guard (vl-reportcard-p x).
Returns: types — Typically includes many duplicates.
Type (symbol-listp types).

Definitions and Theorems

Function: vl-reportcard-types

(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: symbol-listp-of-vl-reportcard-types

(defthm symbol-listp-of-vl-reportcard-types
  (b* ((types (vl-reportcard-types x)))
    (symbol-listp types))
  :rule-classes :rewrite)

Theorem: vl-reportcard-types-of-vl-reportcard-fix-x

(defthm vl-reportcard-types-of-vl-reportcard-fix-x
  (equal (vl-reportcard-types (vl-reportcard-fix x))
         (vl-reportcard-types x)))

Theorem: vl-reportcard-types-vl-reportcard-equiv-congruence-on-x

(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)