(vl-selexpr-welltyped-p x) → *
Function:
(defun vl-selexpr-welltyped-p (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (not (vl-atom-p x)))) (let ((__function__ 'vl-selexpr-welltyped-p)) (declare (ignorable __function__)) (b* (((vl-nonatom x) x)) (and x.finaltype (posp x.finalwidth)))))
Theorem:
(defthm vl-selexpr-welltyped-p-of-vl-expr-fix-x (equal (vl-selexpr-welltyped-p (vl-expr-fix x)) (vl-selexpr-welltyped-p x)))
Theorem:
(defthm vl-selexpr-welltyped-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-selexpr-welltyped-p x) (vl-selexpr-welltyped-p x-equiv))) :rule-classes :congruence)