		Search-engine friendly clone of the ACL2 documentation.

Clean-warnings

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)

Subtopics

Vl-warning-sort: Mergesort warnings using vl-warning-<