(vl-expr-is-extensional x) → *
Function:
(defun vl-expr-is-extensional (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr-is-extensional)) (declare (ignorable __function__)) (vl-expr-case x :vl-literal (vl-value-case x.val :vl-extint) :vl-qmark (and (vl-expr-is-extensional x.then) (vl-expr-is-extensional x.else)) :otherwise nil)))
Theorem:
(defthm vl-expr-is-extensional-of-vl-expr-fix-x (equal (vl-expr-is-extensional (vl-expr-fix x)) (vl-expr-is-extensional x)))
Theorem:
(defthm vl-expr-is-extensional-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-is-extensional x) (vl-expr-is-extensional x-equiv))) :rule-classes :congruence)