		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-modinst-warnings

Signature
(vl-duplicate-modinst-warnings dupes fixed orig modname) → warnings
Arguments: dupes — The modinsts that were duplicated. (fixed).
Guard (vl-modinstlist-p dupes).; fixed — Fixed versions of orig.
Guard (vl-modinstlist-p fixed).; orig — Original mod instances, i.e., before fixing.
Guard (vl-modinstlist-p orig).; modname — Guard (stringp modname).
Returns: warnings — Warnings for each duplicate modinst.
Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-duplicate-modinst-warnings

(defun vl-duplicate-modinst-warnings (dupes fixed orig modname)
 (declare (xargs :guard (and (vl-modinstlist-p dupes)
                             (vl-modinstlist-p fixed)
                             (vl-modinstlist-p orig)
                             (stringp modname))))
 (declare (xargs :guard (same-lengthp fixed orig)))
 (let ((__function__ 'vl-duplicate-modinst-warnings))
  (declare (ignorable __function__))
  (b*
   (((when (atom dupes)) nil)
    (locs (vl-duplicate-modinst-locations (car dupes)
                                          fixed orig))
    (warning
        (vl-make-duplicate-warning "module instances" locs modname))
    (rest (vl-duplicate-modinst-warnings (cdr dupes)
                                         fixed orig modname)))
   (cons warning rest))))

Theorem: vl-warninglist-p-of-vl-duplicate-modinst-warnings

(defthm vl-warninglist-p-of-vl-duplicate-modinst-warnings
  (b*
    ((warnings
          (vl-duplicate-modinst-warnings dupes fixed orig modname)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)