		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-make-duplicate-warning

Signature
(vl-make-duplicate-warning type locs modname) → warning
Arguments: type — Guard (stringp type).; locs — Guard (vl-locationlist-p locs).; modname — Guard (stringp modname).
Returns: warning — Type (vl-warning-p warning).

Definitions and Theorems

Function: vl-make-duplicate-warning

(defun vl-make-duplicate-warning (type locs modname)
  (declare (xargs :guard (and (stringp type)
                              (vl-locationlist-p locs)
                              (stringp modname))))
  (let ((__function__ 'vl-make-duplicate-warning))
    (declare (ignorable __function__))
    (b* ((locs (list-fix locs))
         (elide-p (> (len locs) 9))
         (elided-locs (if elide-p (take 9 locs) locs)))
      (make-vl-warning
           :type :vl-warn-duplicates
           :msg (cat "In module ~m0, found duplicated "
                     type " at "
                     (vl-locationlist-string (len elided-locs))
                     (if elide-p " (and other locations)."
                       "."))
           :args (cons modname elided-locs)
           :fatalp nil
           :fn 'vl-make-duplicate-warning))))

Theorem: vl-warning-p-of-vl-make-duplicate-warning

(defthm vl-warning-p-of-vl-make-duplicate-warning
  (b* ((warning (vl-make-duplicate-warning type locs modname)))
    (vl-warning-p warning))
  :rule-classes :rewrite)

Subtopics

Vl-locationlist-string