Top-level duplicate-detect check.
(vl-design-duplicate-detect x) → new-x
Function:
(defun vl-design-duplicate-detect (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-duplicate-detect)) (declare (ignorable __function__)) (b* (((vl-design x)) (ss (vl-scopestack-init x)) (new-mods (vl-modulelist-duplicate-detect x.mods ss))) (vl-scopestacks-free) (clear-memoize-table 'vl-expr-strip) (change-vl-design x :mods new-mods))))
Theorem:
(defthm vl-design-p-of-vl-design-duplicate-detect (b* ((new-x (vl-design-duplicate-detect x))) (vl-design-p new-x)) :rule-classes :rewrite)