(vl-update-paramtype-udims udims x) → new-x
Function:
(defun vl-update-paramtype-udims (udims x) (declare (xargs :guard (and (vl-dimensionlist-p udims) (vl-paramtype-p x)))) (declare (xargs :guard (and (consp udims) (member (vl-paramtype-kind x) '(:vl-implicitvalueparam :vl-explicitvalueparam))))) (let ((__function__ 'vl-update-paramtype-udims)) (declare (ignorable __function__)) (vl-paramtype-case x :vl-implicitvalueparam (b* ((signedp (cond ((not x.sign) nil) ((vl-exprsign-equiv x.sign :vl-signed) t) (t nil))) (pdims (and x.range (list (vl-range->dimension x.range)))) (datatype (make-vl-coretype :name :vl-logic :pdims pdims :signedp signedp :udims udims))) (make-vl-explicitvalueparam :type datatype :default x.default :final-value nil)) :vl-explicitvalueparam (change-vl-explicitvalueparam x :type (vl-datatype-update-udims udims x.type)) :otherwise (progn$ (impossible) (vl-paramtype-fix x)))))
Theorem:
(defthm vl-paramtype-p-of-vl-update-paramtype-udims (b* ((new-x (vl-update-paramtype-udims udims x))) (vl-paramtype-p new-x)) :rule-classes :rewrite)