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