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