		Search-engine friendly clone of the ACL2 documentation.

Check-case

Vl-make-case-equiv-warnings

Signature
(vl-make-case-equiv-warnings names warnings) → warnings
Arguments: names — Guard (string-list-listp names).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-make-case-equiv-warnings

(defun vl-make-case-equiv-warnings (names warnings)
 (declare (xargs :guard (and (string-list-listp names)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-make-case-equiv-warnings))
  (declare (ignorable __function__))
  (b*
   (((when (atom names)) (ok))
    (warnings
     (warn
      :type :vl-warn-case-sensitive-names
      :msg
      "Names differ only by case: ~&0.  This might indicate a typo ~
                             and may also cause problems for some Verilog tools."
      :args (list (string-list-fix (car names))))))
   (vl-make-case-equiv-warnings (cdr names)
                                warnings))))

Theorem: vl-warninglist-p-of-vl-make-case-equiv-warnings

(defthm vl-warninglist-p-of-vl-make-case-equiv-warnings
  (b* ((warnings (vl-make-case-equiv-warnings names warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)