(vl-paramtype-allexprs-nrev x nrev) → nrev
Function:
(defun vl-paramtype-allexprs-nrev$inline (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-paramtype-p x))) (let ((__function__ 'vl-paramtype-allexprs-nrev)) (declare (ignorable __function__)) (b* ((x (vl-paramtype-fix x))) (vl-paramtype-case x (:vl-implicitvalueparam (b* ((nrev (vl-maybe-range-allexprs-nrev x.range nrev))) (vl-maybe-expr-allexprs-nrev x.default nrev))) (:vl-explicitvalueparam (b* ((nrev (vl-datatype-allexprs-nrev x.type nrev))) (vl-maybe-expr-allexprs-nrev x.default nrev))) (:vl-typeparam (vl-maybe-datatype-allexprs-nrev x.default nrev))))))
Theorem:
(defthm vl-paramtype-allexprs-nrev$inline-of-vl-paramtype-fix-x (equal (vl-paramtype-allexprs-nrev$inline (vl-paramtype-fix x) nrev) (vl-paramtype-allexprs-nrev$inline x nrev)))
Theorem:
(defthm vl-paramtype-allexprs-nrev$inline-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-paramtype-allexprs-nrev$inline x nrev) (vl-paramtype-allexprs-nrev$inline x-equiv nrev))) :rule-classes :congruence)