Get the
(vl-expr->finaltype x) → type?
See vl-expr-p for a discussion of types. The result is a vl-maybe-exprtype-p.
Function:
(defun vl-expr->finaltype$inline (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr->finaltype)) (declare (ignorable __function__)) (vl-expr-case x :atom x.finaltype :nonatom x.finaltype)))
Theorem:
(defthm vl-maybe-exprtype-p-of-vl-expr->finaltype (b* ((type? (vl-expr->finaltype$inline x))) (vl-maybe-exprtype-p type?)) :rule-classes ((:rewrite) (:type-prescription :corollary (and (symbolp (vl-expr->finaltype x)) (not (equal (vl-expr->finaltype x) t))))))
Theorem:
(defthm vl-expr->finaltype-of-vl-atom (equal (vl-expr->finaltype (make-vl-atom :guts guts :finalwidth finalwidth :finaltype finaltype :atts atts)) (vl-maybe-exprtype-fix finaltype)))
Theorem:
(defthm vl-expr->finaltype-of-vl-nonatom (equal (vl-expr->finaltype (make-vl-nonatom :op op :atts atts :args args :finalwidth finalwidth :finaltype finaltype)) (vl-maybe-exprtype-fix finaltype)))
Theorem:
(defthm vl-expr->finaltype$inline-of-vl-expr-fix-x (equal (vl-expr->finaltype$inline (vl-expr-fix x)) (vl-expr->finaltype$inline x)))
Theorem:
(defthm vl-expr->finaltype$inline-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr->finaltype$inline x) (vl-expr->finaltype$inline x-equiv))) :rule-classes :congruence)