(vl-exprtype-max x y &rest rst) is given vl-exprtype-ps as arguments;
it returns
Function:
(defun vl-exprtype-max-fn (x y) (declare (xargs :guard (and (vl-exprtype-p x) (vl-exprtype-p y)))) (let ((x-fix (mbe :logic (case (vl-exprtype-fix x) (:vl-signed :vl-signed) (otherwise :vl-unsigned)) :exec x)) (y-fix (mbe :logic (case (vl-exprtype-fix y) (:vl-signed :vl-signed) (otherwise :vl-unsigned)) :exec y))) (if (or (eq x-fix :vl-unsigned) (eq y-fix :vl-unsigned)) :vl-unsigned :vl-signed)))
Theorem:
(defthm vl-exprtype-p-of-vl-exprtype-max (vl-exprtype-p (vl-exprtype-max x y)))
Theorem:
(defthm type-of-vl-exprtype-max (and (symbolp (vl-exprtype-max x y)) (not (equal t (vl-exprtype-max x y))) (not (equal nil (vl-exprtype-max x y)))) :rule-classes :type-prescription)
Theorem:
(defthm vl-exprtype-max-of-vl-exprtype-max (equal (vl-exprtype-max (vl-exprtype-max x y) z) (vl-exprtype-max x (vl-exprtype-max y z))))
Theorem:
(defthm vl-exprtype-max-fn-of-vl-exprtype-fix-x (equal (vl-exprtype-max-fn (vl-exprtype-fix x) y) (vl-exprtype-max-fn x y)))
Theorem:
(defthm vl-exprtype-max-fn-vl-exprtype-equiv-congruence-on-x (implies (vl-exprtype-equiv x x-equiv) (equal (vl-exprtype-max-fn x y) (vl-exprtype-max-fn x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm vl-exprtype-max-fn-of-vl-exprtype-fix-y (equal (vl-exprtype-max-fn x (vl-exprtype-fix y)) (vl-exprtype-max-fn x y)))
Theorem:
(defthm vl-exprtype-max-fn-vl-exprtype-equiv-congruence-on-y (implies (vl-exprtype-equiv y y-equiv) (equal (vl-exprtype-max-fn x y) (vl-exprtype-max-fn x y-equiv))) :rule-classes :congruence)