Maximum mathematical integer value of type
This depends on the implementation environment.
Function:
(defun sint-max (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'sint-max)) (declare (ignorable __function__)) (1- (expt 2 (1- (* 8 (ienv->int-bytes ienv)))))))
Theorem:
(defthm natp-of-sint-max (b* ((val (sint-max ienv))) (natp val)) :rule-classes (:rewrite :type-prescription))