(vl-module-dupeinst-check x ss) → new-x
Function:
(defun vl-module-dupeinst-check (x ss) (declare (xargs :guard (and (vl-module-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-module-dupeinst-check)) (declare (ignorable __function__)) (b* (((vl-module x) x) (- (and *dupeinst-check-debug* (cw "Dupeinst checking ~s0~%" x.name))) (ss (vl-scopestack-push x ss)) (modinsts (vl-module->flatten-modinsts x)) (alist (vl-make-dupeinst-alist modinsts)) (warnings (vl-warnings-for-dupeinst-alist alist ss x.warnings))) (change-vl-module x :warnings warnings))))
Theorem:
(defthm vl-module-p-of-vl-module-dupeinst-check (b* ((new-x (vl-module-dupeinst-check x ss))) (vl-module-p new-x)) :rule-classes :rewrite)