		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-alwayslist-check-style

Signature
(vl-alwayslist-check-style x warnings) → warnings
Arguments: x — Guard (vl-alwayslist-p x).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-alwayslist-check-style

(defun vl-alwayslist-check-style (x warnings)
  (declare (xargs :guard (and (vl-alwayslist-p x)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-alwayslist-check-style))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (ok))
         (warnings (vl-always-check-style (first x)
                                          warnings)))
      (vl-alwayslist-check-style (rest x)
                                 warnings))))

Theorem: vl-warninglist-p-of-vl-alwayslist-check-style

(defthm vl-warninglist-p-of-vl-alwayslist-check-style
  (b* ((warnings (vl-alwayslist-check-style x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)