		Search-engine friendly clone of the ACL2 documentation.

Nameclash

Vl-make-nameclash-warnings

Signature
(vl-make-nameclash-warnings scopename clashnames locals imports warnings) → new-warning
Arguments: scopename — Guard (vl-maybe-scopeid-p scopename).; clashnames — The names that have clashes in this scope.
Guard (string-listp clashnames).; locals — Guard (vl-scopeitem-alist-p locals).; imports — Guard (vl-importresult-alist-p imports).; warnings — Guard (vl-warninglist-p warnings).
Returns: new-warning — Type (vl-warninglist-p new-warning).

Definitions and Theorems

Function: vl-make-nameclash-warnings

(defun vl-make-nameclash-warnings
       (scopename clashnames locals imports warnings)
 (declare (xargs :guard (and (vl-maybe-scopeid-p scopename)
                             (string-listp clashnames)
                             (vl-scopeitem-alist-p locals)
                             (vl-importresult-alist-p imports)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-make-nameclash-warnings))
   (declare (ignorable __function__))
   (b*
    (((when (atom clashnames)) (ok))
     (warnings (vl-make-nameclash-warning scopename (car clashnames)
                                          locals imports warnings)))
    (vl-make-nameclash-warnings scopename (cdr clashnames)
                                locals imports warnings))))

Theorem: vl-warninglist-p-of-vl-make-nameclash-warnings

(defthm vl-warninglist-p-of-vl-make-nameclash-warnings
  (b* ((new-warning (vl-make-nameclash-warnings
                         scopename
                         clashnames locals imports warnings)))
    (vl-warninglist-p new-warning))
  :rule-classes :rewrite)

Theorem: vl-make-nameclash-warnings-of-vl-maybe-scopeid-fix-scopename

(defthm vl-make-nameclash-warnings-of-vl-maybe-scopeid-fix-scopename
 (equal
   (vl-make-nameclash-warnings (vl-maybe-scopeid-fix scopename)
                               clashnames locals imports warnings)
   (vl-make-nameclash-warnings scopename
                               clashnames locals imports warnings)))

Theorem: vl-make-nameclash-warnings-vl-maybe-scopeid-equiv-congruence-on-scopename

(defthm
 vl-make-nameclash-warnings-vl-maybe-scopeid-equiv-congruence-on-scopename
 (implies
  (vl-maybe-scopeid-equiv scopename scopename-equiv)
  (equal
   (vl-make-nameclash-warnings scopename
                               clashnames locals imports warnings)
   (vl-make-nameclash-warnings scopename-equiv
                               clashnames locals imports warnings)))
 :rule-classes :congruence)

Theorem: vl-make-nameclash-warnings-of-string-list-fix-clashnames

(defthm vl-make-nameclash-warnings-of-string-list-fix-clashnames
 (equal
  (vl-make-nameclash-warnings scopename (string-list-fix clashnames)
                              locals imports warnings)
  (vl-make-nameclash-warnings scopename
                              clashnames locals imports warnings)))

Theorem: vl-make-nameclash-warnings-string-list-equiv-congruence-on-clashnames

(defthm
 vl-make-nameclash-warnings-string-list-equiv-congruence-on-clashnames
 (implies
  (str::string-list-equiv clashnames clashnames-equiv)
  (equal
     (vl-make-nameclash-warnings scopename
                                 clashnames locals imports warnings)
     (vl-make-nameclash-warnings scopename clashnames-equiv
                                 locals imports warnings)))
 :rule-classes :congruence)

Theorem: vl-make-nameclash-warnings-of-vl-scopeitem-alist-fix-locals

(defthm vl-make-nameclash-warnings-of-vl-scopeitem-alist-fix-locals
 (equal
   (vl-make-nameclash-warnings scopename clashnames
                               (vl-scopeitem-alist-fix locals)
                               imports warnings)
   (vl-make-nameclash-warnings scopename
                               clashnames locals imports warnings)))

Theorem: vl-make-nameclash-warnings-vl-scopeitem-alist-equiv-congruence-on-locals

(defthm
 vl-make-nameclash-warnings-vl-scopeitem-alist-equiv-congruence-on-locals
 (implies
  (vl-scopeitem-alist-equiv locals locals-equiv)
  (equal
     (vl-make-nameclash-warnings scopename
                                 clashnames locals imports warnings)
     (vl-make-nameclash-warnings scopename clashnames
                                 locals-equiv imports warnings)))
 :rule-classes :congruence)

Theorem: vl-make-nameclash-warnings-of-vl-importresult-alist-fix-imports

(defthm
    vl-make-nameclash-warnings-of-vl-importresult-alist-fix-imports
 (equal
   (vl-make-nameclash-warnings scopename clashnames locals
                               (vl-importresult-alist-fix imports)
                               warnings)
   (vl-make-nameclash-warnings scopename
                               clashnames locals imports warnings)))

Theorem: vl-make-nameclash-warnings-vl-importresult-alist-equiv-congruence-on-imports

(defthm
 vl-make-nameclash-warnings-vl-importresult-alist-equiv-congruence-on-imports
 (implies
  (vl-importresult-alist-equiv imports imports-equiv)
  (equal
     (vl-make-nameclash-warnings scopename
                                 clashnames locals imports warnings)
     (vl-make-nameclash-warnings scopename clashnames
                                 locals imports-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-make-nameclash-warnings-of-vl-warninglist-fix-warnings

(defthm vl-make-nameclash-warnings-of-vl-warninglist-fix-warnings
 (equal
  (vl-make-nameclash-warnings scopename clashnames locals
                              imports (vl-warninglist-fix warnings))
  (vl-make-nameclash-warnings scopename
                              clashnames locals imports warnings)))

Theorem: vl-make-nameclash-warnings-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-make-nameclash-warnings-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
     (vl-make-nameclash-warnings scopename
                                 clashnames locals imports warnings)
     (vl-make-nameclash-warnings scopename clashnames
                                 locals imports warnings-equiv)))
 :rule-classes :congruence)