(vl-operandinfo-signedness-caveat x) → *
Function:
(defun vl-operandinfo-signedness-caveat (x) (declare (xargs :guard (vl-operandinfo-p x))) (let ((__function__ 'vl-operandinfo-signedness-caveat)) (declare (ignorable __function__)) (b* (((vl-operandinfo x))) (and (vl-partselect-case x.part :none) (consp x.seltrace) (vl-selstep->caveat (car x.seltrace))))))
Theorem:
(defthm vl-operandinfo-signedness-caveat-of-vl-operandinfo-fix-x (equal (vl-operandinfo-signedness-caveat (vl-operandinfo-fix x)) (vl-operandinfo-signedness-caveat x)))
Theorem:
(defthm vl-operandinfo-signedness-caveat-vl-operandinfo-equiv-congruence-on-x (implies (vl-operandinfo-equiv x x-equiv) (equal (vl-operandinfo-signedness-caveat x) (vl-operandinfo-signedness-caveat x-equiv))) :rule-classes :congruence)