		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Sint-min

Minimum ACL2 integer value of type signed int.

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

Definitions and Theorems

Function: sint-min

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

Theorem: integerp-of-sint-min

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

Theorem: sint-min-bound

(defthm sint-min-bound
  (<= (sint-min) -32768)
  :rule-classes :linear)

Subtopics

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