		Search-engine friendly clone of the ACL2 documentation.

Vl-clean-warnings

Sort and remove duplicates from a list of warnings.

Signature
(vl-clean-warnings x) → ans
Arguments: x — Guard (vl-warninglist-p x).
Returns: ans — Type (vl-warninglist-p ans).

Definitions and Theorems

Function: vl-clean-warnings

(defun vl-clean-warnings (x)
  (declare (xargs :guard (vl-warninglist-p x)))
  (let ((__function__ 'vl-clean-warnings))
    (declare (ignorable __function__))
    (acl2::remove-adjacent-duplicates
         (vl-warning-sort (list-fix (vl-warninglist-fix x))))))

Theorem: vl-warninglist-p-of-vl-clean-warnings

(defthm vl-warninglist-p-of-vl-clean-warnings
  (b* ((ans (vl-clean-warnings x)))
    (vl-warninglist-p ans))
  :rule-classes :rewrite)

Theorem: vl-clearn-warnings-under-iff

(defthm vl-clearn-warnings-under-iff
  (iff (vl-clean-warnings x) (consp x)))

Theorem: vl-clean-warnings-of-vl-warninglist-fix-x

(defthm vl-clean-warnings-of-vl-warninglist-fix-x
  (equal (vl-clean-warnings (vl-warninglist-fix x))
         (vl-clean-warnings x)))

Theorem: vl-clean-warnings-vl-warninglist-equiv-congruence-on-x

(defthm vl-clean-warnings-vl-warninglist-equiv-congruence-on-x
  (implies (vl-warninglist-equiv x x-equiv)
           (equal (vl-clean-warnings x)
                  (vl-clean-warnings x-equiv)))
  :rule-classes :congruence)