(vl-expr->maybe-subtype x) → subtype
Function:
(defun vl-expr->maybe-subtype (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr->maybe-subtype)) (declare (ignorable __function__)) (vl-expr-case x :vl-literal nil :vl-index nil :vl-unary nil :vl-binary nil :vl-qmark nil :vl-concat nil :vl-multiconcat nil :vl-mintypmax nil :vl-call x.typearg :vl-stream nil :vl-cast nil :vl-inside nil :vl-tagged nil :vl-pattern x.pattype :vl-special nil :vl-eventexpr nil :vl-bitselect-expr nil :vl-partselect-expr nil)))
Theorem:
(defthm vl-maybe-datatype-p-of-vl-expr->maybe-subtype (b* ((subtype (vl-expr->maybe-subtype x))) (vl-maybe-datatype-p subtype)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-datatype-count-of-vl-expr->maybe-subtype (b* ((?subtype (vl-expr->maybe-subtype x))) (< (vl-maybe-datatype-count subtype) (vl-expr-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-expr->maybe-subtype-of-vl-expr-fix-x (equal (vl-expr->maybe-subtype (vl-expr-fix x)) (vl-expr->maybe-subtype x)))
Theorem:
(defthm vl-expr->maybe-subtype-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr->maybe-subtype x) (vl-expr->maybe-subtype x-equiv))) :rule-classes :congruence)