		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-add-lost-module-warning

Signature
(vl-add-lost-module-warning x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x).

Definitions and Theorems

Function: vl-add-lost-module-warning

(defun vl-add-lost-module-warning (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-add-lost-module-warning))
  (declare (ignorable __function__))
  (b*
   (((vl-module x))
    (warnings x.warnings)
    (warnings
     (fatal
      :type :vl-unreachable-module
      :msg
      "After elaboration ~s0 became unreachable. This ~
                              is typically due to errors in the modules that ~
                              instantiate it.  We will keep the ~
                              pre-elaboration version of this module, but ~
                              beware: this may not be entirely sensible."
      :args (list x.name))))
   (change-vl-module x
                     :warnings warnings))))

Theorem: vl-module-p-of-vl-add-lost-module-warning

(defthm vl-module-p-of-vl-add-lost-module-warning
  (b* ((new-x (vl-add-lost-module-warning x)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Theorem: vl-add-lost-module-warning-of-vl-module-fix-x

(defthm vl-add-lost-module-warning-of-vl-module-fix-x
  (equal (vl-add-lost-module-warning (vl-module-fix x))
         (vl-add-lost-module-warning x)))

Theorem: vl-add-lost-module-warning-vl-module-equiv-congruence-on-x

(defthm vl-add-lost-module-warning-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-add-lost-module-warning x)
                  (vl-add-lost-module-warning x-equiv)))
  :rule-classes :congruence)