(vl-design-use-set-report x omit) → (mv new-x report)
Function:
(defun vl-design-use-set-report (x omit) (declare (xargs :guard (and (vl-design-p x) (string-listp omit)))) (let ((__function__ 'vl-design-use-set-report)) (declare (ignorable __function__)) (b* ((x (vl-design-fix x)) (omit (mbe :logic (if (string-listp omit) omit nil) :exec omit)) ((vl-design x) x) ((mv new-mods report) (vl-mark-wires-for-modulelist x.mods omit)) (new-x (change-vl-design x :mods new-mods))) (mv new-x report))))
Theorem:
(defthm vl-design-p-of-vl-design-use-set-report.new-x (b* (((mv ?new-x ?report) (vl-design-use-set-report x omit))) (vl-design-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-useset-report-p-of-vl-design-use-set-report.report (b* (((mv ?new-x ?report) (vl-design-use-set-report x omit))) (vl-useset-report-p report)) :rule-classes :rewrite)