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