		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Slong-min

Minimum ACL2 integer value of type signed long.

Signature
(slong-min) → slong-min
Returns: slong-min — Type (integerp slong-min).

Definitions and Theorems

Function: slong-min

(defun slong-min nil
  (declare (xargs :guard t))
  (let ((__function__ 'slong-min))
    (declare (ignorable __function__))
    (- (expt 2 (1- (long-bits))))))

Theorem: integerp-of-slong-min

(defthm integerp-of-slong-min
  (b* ((slong-min (slong-min)))
    (integerp slong-min))
  :rule-classes :type-prescription)

Theorem: slong-min-bound

(defthm slong-min-bound
  (<= (slong-min) -2147483648)
  :rule-classes :linear)

Subtopics

Slong-min-<=-sint-min: General relation between signed long and signed int minima.
Slong-min-vs-sllong-min: Relation between signed long and signed long long minima.
Sllong-min-<=-slong-min: General relation between signed long long and signed long minima.
Sint-min-vs-slong-min: Relation between signed int and signed long minima.