		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-possible-typo-warnings

Signature
(vl-possible-typo-warnings typo-alist) → warnings
Arguments: typo-alist — Guard (alistp typo-alist).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-possible-typo-warnings

(defun vl-possible-typo-warnings (typo-alist)
 (declare (xargs :guard (alistp typo-alist)))
 (declare (xargs :guard (and (vl-string-keys-p typo-alist)
                             (vl-string-list-values-p typo-alist))))
 (let ((__function__ 'vl-possible-typo-warnings))
   (declare (ignorable __function__))
   (b*
    (((when (atom typo-alist)) nil)
     ((cons badwire good-alternatives)
      (car typo-alist))
     (w (make-vl-warning
             :type :vl-warn-possible-typo
             :msg "Possible typo: implicit wire ~s0 looks like ~&1."
             :args (list badwire good-alternatives)
             :fn __function__
             :fatalp nil)))
    (cons w
          (vl-possible-typo-warnings (cdr typo-alist))))))

Theorem: vl-warninglist-p-of-vl-possible-typo-warnings

(defthm vl-warninglist-p-of-vl-possible-typo-warnings
  (b* ((warnings (vl-possible-typo-warnings typo-alist)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)