(vl-make-nameclash-warning scopename clashname locals imports warnings) → new-warning
Function:
(defun vl-make-nameclash-warning (scopename clashname locals imports warnings) (declare (xargs :guard (and (vl-maybe-scopeid-p scopename) (stringp clashname) (vl-scopeitem-alist-p locals) (vl-importresult-alist-p imports) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-make-nameclash-warning)) (declare (ignorable __function__)) (b* ((scopename (vl-maybe-scopeid-fix scopename))) (fatal :type :vl-name-clash :msg "In ~@0: ~s1" :args (list (cond ((stringp scopename) (vmsg scopename)) ((integerp scopename) (vmsg "generate loop ~x0" scopename)) (t (vmsg "Unnamed scope"))) (vl-nameclash-warning-summary clashname locals imports))))))
Theorem:
(defthm vl-warninglist-p-of-vl-make-nameclash-warning (b* ((new-warning (vl-make-nameclash-warning scopename clashname locals imports warnings))) (vl-warninglist-p new-warning)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-nameclash-warning-of-vl-maybe-scopeid-fix-scopename (equal (vl-make-nameclash-warning (vl-maybe-scopeid-fix scopename) clashname locals imports warnings) (vl-make-nameclash-warning scopename clashname locals imports warnings)))
Theorem:
(defthm vl-make-nameclash-warning-vl-maybe-scopeid-equiv-congruence-on-scopename (implies (vl-maybe-scopeid-equiv scopename scopename-equiv) (equal (vl-make-nameclash-warning scopename clashname locals imports warnings) (vl-make-nameclash-warning scopename-equiv clashname locals imports warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-nameclash-warning-of-str-fix-clashname (equal (vl-make-nameclash-warning scopename (str-fix clashname) locals imports warnings) (vl-make-nameclash-warning scopename clashname locals imports warnings)))
Theorem:
(defthm vl-make-nameclash-warning-streqv-congruence-on-clashname (implies (streqv clashname clashname-equiv) (equal (vl-make-nameclash-warning scopename clashname locals imports warnings) (vl-make-nameclash-warning scopename clashname-equiv locals imports warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-nameclash-warning-of-vl-scopeitem-alist-fix-locals (equal (vl-make-nameclash-warning scopename clashname (vl-scopeitem-alist-fix locals) imports warnings) (vl-make-nameclash-warning scopename clashname locals imports warnings)))
Theorem:
(defthm vl-make-nameclash-warning-vl-scopeitem-alist-equiv-congruence-on-locals (implies (vl-scopeitem-alist-equiv locals locals-equiv) (equal (vl-make-nameclash-warning scopename clashname locals imports warnings) (vl-make-nameclash-warning scopename clashname locals-equiv imports warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-nameclash-warning-of-vl-importresult-alist-fix-imports (equal (vl-make-nameclash-warning scopename clashname locals (vl-importresult-alist-fix imports) warnings) (vl-make-nameclash-warning scopename clashname locals imports warnings)))
Theorem:
(defthm vl-make-nameclash-warning-vl-importresult-alist-equiv-congruence-on-imports (implies (vl-importresult-alist-equiv imports imports-equiv) (equal (vl-make-nameclash-warning scopename clashname locals imports warnings) (vl-make-nameclash-warning scopename clashname locals imports-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-nameclash-warning-of-vl-warninglist-fix-warnings (equal (vl-make-nameclash-warning scopename clashname locals imports (vl-warninglist-fix warnings)) (vl-make-nameclash-warning scopename clashname locals imports warnings)))
Theorem:
(defthm vl-make-nameclash-warning-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-make-nameclash-warning scopename clashname locals imports warnings) (vl-make-nameclash-warning scopename clashname locals imports warnings-equiv))) :rule-classes :congruence)