(vl-design-qmarksize-check x) → new-x
Function:
(defun vl-design-qmarksize-check (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-qmarksize-check)) (declare (ignorable __function__)) (b* (((vl-design x)) (ss (vl-scopestack-init (vl-design-fix x))) (mods (vl-modulelist-qmarksize-check x.mods ss)) (ifs (vl-interfacelist-qmarksize-check x.interfaces ss)) (pkgs (vl-packagelist-qmarksize-check x.packages ss)) (warnings (append (vl-ctxexprlist-qmarksize-check (vl-design-toplevel-ctxexprs x)) x.warnings))) (change-vl-design x :mods mods :interfaces ifs :packages pkgs :warnings warnings))))
Theorem:
(defthm vl-design-p-of-vl-design-qmarksize-check (b* ((new-x (vl-design-qmarksize-check x))) (vl-design-p new-x)) :rule-classes :rewrite)