		Search-engine friendly clone of the ACL2 documentation.

Check-case

Vl-module-check-case

Signature
(vl-module-check-case x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Maybe with new warnings.
Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-check-case

(defun vl-module-check-case (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-check-case))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    (names (append (vl-portdecllist->names x.portdecls)
                   (vl-module->modnamespace x)))
    (names (cwtime (mergesort names)
                   :name check-case-gather-names
                   :mintime 1/2))
    (equiv-names (cwtime (vl-find-case-equivalent-strings names)
                         :name check-case-find-equiv-strs
                         :mintime 1/2))
    ((unless equiv-names) x)
    (warnings (vl-make-case-equiv-warnings equiv-names x.warnings)))
   (change-vl-module x
                     :warnings warnings))))

Theorem: vl-module-p-of-vl-module-check-case

(defthm vl-module-p-of-vl-module-check-case
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-check-case x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)