		Search-engine friendly clone of the ACL2 documentation.

Dupeinst-check

Vl-warnings-for-dupeinst-alist

Signature
(vl-warnings-for-dupeinst-alist alist ss warnings) → new-warnings
Arguments: alist — Guard (vl-dupeinst-alistp alist).; ss — Guard (vl-scopestack-p ss).; warnings — Guard (vl-warninglist-p warnings).
Returns: new-warnings — Type (vl-warninglist-p new-warnings).

Definitions and Theorems

Function: vl-warnings-for-dupeinst-alist

(defun vl-warnings-for-dupeinst-alist (alist ss warnings)
 (declare (xargs :guard (and (vl-dupeinst-alistp alist)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-warnings-for-dupeinst-alist))
   (declare (ignorable __function__))
   (b* (((when (atom alist)) (ok))
        (rhs (caar alist))
        (assigns (cdar alist))
        (warnings (vl-maybe-warn-dupeinst rhs assigns ss warnings)))
     (vl-warnings-for-dupeinst-alist (cdr alist)
                                     ss warnings))))

Theorem: vl-warninglist-p-of-vl-warnings-for-dupeinst-alist

(defthm vl-warninglist-p-of-vl-warnings-for-dupeinst-alist
  (b* ((new-warnings
            (vl-warnings-for-dupeinst-alist alist ss warnings)))
    (vl-warninglist-p new-warnings))
  :rule-classes :rewrite)