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