		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-lint-apply-quiet

Signature
(vl-lint-apply-quiet quiet design) → new-design
Arguments: quiet — Guard (string-listp quiet).; design — Guard (vl-design-p design).
Returns: new-design — Type (vl-design-p new-design).

Definitions and Theorems

Function: vl-lint-apply-quiet

(defun vl-lint-apply-quiet (quiet design)
  (declare (xargs :guard (and (string-listp quiet)
                              (vl-design-p design))))
  (let ((__function__ 'vl-lint-apply-quiet))
    (declare (ignorable __function__))
    (b* ((design (vl-design-fix design))
         (mods (vl-design->mods design))
         (mods (vl-delete-modules quiet mods)))
      (change-vl-design design :mods mods))))

Theorem: vl-design-p-of-vl-lint-apply-quiet

(defthm vl-design-p-of-vl-lint-apply-quiet
  (b* ((new-design (vl-lint-apply-quiet quiet design)))
    (vl-design-p new-design))
  :rule-classes :rewrite)