		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-warninglist-keep-suppressed

Signature
(vl-warninglist-keep-suppressed x) → new-x
Arguments: x — Guard (vl-warninglist-p x).
Returns: new-x — Type (vl-warninglist-p new-x).

Definitions and Theorems

Function: vl-warninglist-keep-suppressed

(defun vl-warninglist-keep-suppressed (x)
  (declare (xargs :guard (vl-warninglist-p x)))
  (let ((__function__ 'vl-warninglist-keep-suppressed))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (vl-warning->suppressedp (car x))
          (cons (vl-warning-fix (car x))
                (vl-warninglist-keep-suppressed (cdr x)))
        (vl-warninglist-keep-suppressed (cdr x))))))

Theorem: vl-warninglist-p-of-vl-warninglist-keep-suppressed

(defthm vl-warninglist-p-of-vl-warninglist-keep-suppressed
  (b* ((new-x (vl-warninglist-keep-suppressed x)))
    (vl-warninglist-p new-x))
  :rule-classes :rewrite)