		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-vardecllist-svbad-warnings

Signature
(vl-vardecllist-svbad-warnings x warnings) → warnings
Arguments: x — Guard (vl-vardecllist-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-vardecllist-svbad-warnings

(defun vl-vardecllist-svbad-warnings (x warnings)
  (declare (xargs :guard (and (vl-vardecllist-p x)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-vardecllist-svbad-warnings))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (ok))
         (warnings (vl-vardecl-svbad-warnings (car x)
                                              warnings)))
      (vl-vardecllist-svbad-warnings (cdr x)
                                     warnings))))

Theorem: vl-warninglist-p-of-vl-vardecllist-svbad-warnings

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