		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Sint-max

Maximum ACL2 integer value of type signed int.

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

Definitions and Theorems

Function: sint-max

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

Theorem: integerp-of-sint-max

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

Theorem: sint-max-bound

(defthm sint-max-bound
  (>= (sint-max) 32767)
  :rule-classes :linear)

Subtopics

Ushort-max-vs-sint-max: Relation between unsigned short and signed int maxima.
Uchar-max-vs-sint-max: Relation between unsigned char and signed int maxima.
Sshort-max-<=-sint-max: General relation between signed short and signed int maxima.
Sshort-max-vs-sint-max: Relation between signed short and signed int maxima.
Sint-max-<=-slong-max: General relation between signed int and signed long maxima.
Sint-max-vs-slong-max: Relation between signed int and signed long maxima.