		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-module-alwaysstyle

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

Definitions and Theorems

Function: vl-module-alwaysstyle

(defun vl-module-alwaysstyle (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-alwaysstyle))
   (declare (ignorable __function__))
   (b*
    ((genblob (vl-module->genblob x))
     (warnings
          (vl-genblob-alwaysstyle genblob (vl-module->warnings x))))
    (change-vl-module x
                      :warnings warnings))))

Theorem: vl-module-p-of-vl-module-alwaysstyle

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