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