		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-modulelist-add-svbad-warnings

Signature
(vl-modulelist-add-svbad-warnings x good bad) → (mv good bad)
Arguments: x — Guard (vl-modulelist-p x).; good — Guard (vl-modulelist-p good).; bad — Guard (vl-modulelist-p bad).
Returns: good — Type (vl-modulelist-p good).; bad — Type (vl-modulelist-p bad).

Definitions and Theorems

Function: vl-modulelist-add-svbad-warnings

(defun vl-modulelist-add-svbad-warnings (x good bad)
  (declare (xargs :guard (and (vl-modulelist-p x)
                              (vl-modulelist-p good)
                              (vl-modulelist-p bad))))
  (let ((__function__ 'vl-modulelist-add-svbad-warnings))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv (vl-modulelist-fix good)
              (vl-modulelist-fix bad)))
         ((mv good bad)
          (vl-module-add-svbad-warnings (first x)
                                        good bad)))
      (vl-modulelist-add-svbad-warnings (rest x)
                                        good bad))))

Theorem: vl-modulelist-p-of-vl-modulelist-add-svbad-warnings.good

(defthm vl-modulelist-p-of-vl-modulelist-add-svbad-warnings.good
  (b* (((mv ?good ?bad)
        (vl-modulelist-add-svbad-warnings x good bad)))
    (vl-modulelist-p good))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-modulelist-add-svbad-warnings.bad

(defthm vl-modulelist-p-of-vl-modulelist-add-svbad-warnings.bad
  (b* (((mv ?good ?bad)
        (vl-modulelist-add-svbad-warnings x good bad)))
    (vl-modulelist-p bad))
  :rule-classes :rewrite)