(vl-value-typedecide x) → class
Function:
(defun vl-value-typedecide (x) (declare (xargs :guard (vl-value-p x))) (let ((__function__ 'vl-value-typedecide)) (declare (ignorable __function__)) (vl-value-case x :vl-constint (vl-exprsign->arithclass x.origsign) :vl-weirdint (vl-exprsign->arithclass x.origsign) :vl-extint :vl-unsigned-int-class :vl-real :vl-real-class :vl-time :vl-real-class :vl-string :vl-unsigned-int-class)))
Theorem:
(defthm vl-arithclass-p-of-vl-value-typedecide (b* ((class (vl-value-typedecide x))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-value-typedecide-of-vl-value-fix-x (equal (vl-value-typedecide (vl-value-fix x)) (vl-value-typedecide x)))
Theorem:
(defthm vl-value-typedecide-vl-value-equiv-congruence-on-x (implies (vl-value-equiv x x-equiv) (equal (vl-value-typedecide x) (vl-value-typedecide x-equiv))) :rule-classes :congruence)