Get the default value from any vl-paramtype-p.
(vl-paramtype->default x) → value
Function:
(defun vl-paramtype->default (x) (declare (xargs :guard (vl-paramtype-p x))) (let ((__function__ 'vl-paramtype->default)) (declare (ignorable __function__)) (vl-paramtype-case x (:vl-implicitvalueparam (and x.default (vl-paramvalue-expr x.default))) (:vl-explicitvalueparam (and x.default (vl-paramvalue-expr x.default))) (:vl-typeparam (and x.default (vl-paramvalue-type x.default))))))
Theorem:
(defthm vl-maybe-paramvalue-p-of-vl-paramtype->default (b* ((value (vl-paramtype->default x))) (vl-maybe-paramvalue-p value)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramtype->default-of-vl-paramtype-fix-x (equal (vl-paramtype->default (vl-paramtype-fix x)) (vl-paramtype->default x)))
Theorem:
(defthm vl-paramtype->default-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-paramtype->default x) (vl-paramtype->default x-equiv))) :rule-classes :congruence)