		Search-engine friendly clone of the ACL2 documentation.

Slong-min

Minimum ACL2 integer value of type signed long.

Function: slong-min

(defun slong-min nil
  (declare (xargs :guard t))
  (- (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)

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.