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