Maximum mathematical integer value of the type
This is either schar-max or uchar-max, based on the flag in the implementation environment.
Function:
(defun char-max (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'char-max)) (declare (ignorable __function__)) (if (ienv->plain-char-signedp ienv) (schar-max) (uchar-max))))
Theorem:
(defthm integerp-of-char-max (b* ((val (char-max ienv))) (integerp val)) :rule-classes :rewrite)
Theorem:
(defthm char-max-of-ienv-fix-ienv (equal (char-max (ienv-fix ienv)) (char-max ienv)))
Theorem:
(defthm char-max-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (char-max ienv) (char-max ienv-equiv))) :rule-classes :congruence)