		Search-engine friendly clone of the ACL2 documentation.

Problem-modules

Vl-design-problem-mods

Remove user-specified problem modules from the design.

Signature
(vl-design-problem-mods design problems) → new-design
Arguments: design — Guard (vl-design-p design).; problems — Guard (string-listp problems).
Returns: new-design — Type (vl-design-p new-design).

Definitions and Theorems

Function: vl-design-problem-mods

(defun vl-design-problem-mods (design problems)
 (declare (xargs :guard (and (vl-design-p design)
                             (string-listp problems))))
 (let ((__function__ 'vl-design-problem-mods))
  (declare (ignorable __function__))
  (b* ((design (vl-design-fix design))
       ((vl-design design) design)
       (new-mods (vl-warn-problem-modulelist design.mods problems)))
    (change-vl-design design
                      :mods new-mods))))

Theorem: vl-design-p-of-vl-design-problem-mods

(defthm vl-design-p-of-vl-design-problem-mods
  (b* ((new-design (vl-design-problem-mods design problems)))
    (vl-design-p new-design))
  :rule-classes :rewrite)