Minimum ACL2 integer value of type
(sllong-min) → sllong-min
Function:
(defun sllong-min nil (declare (xargs :guard t)) (let ((__function__ 'sllong-min)) (declare (ignorable __function__)) (- (expt 2 (1- (llong-bits))))))
Theorem:
(defthm integerp-of-sllong-min (b* ((sllong-min (sllong-min))) (integerp sllong-min)) :rule-classes :type-prescription)
Theorem:
(defthm sllong-min-bound (<= (sllong-min) -9223372036854775808) :rule-classes :linear)