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 x.default) (:vl-explicitvalueparam x.default) (:vl-typeparam 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-forward (or (not (vl-paramtype->default x)) (vl-expr-p (vl-paramtype->default x)) (vl-datatype-p (vl-paramtype->default x))) :rule-classes ((:forward-chaining :trigger-terms ((vl-paramtype->default x)))))
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)