		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Sllong-max

Maximum ACL2 integer value of type signed long long.

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

Definitions and Theorems

Function: sllong-max

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

Theorem: integerp-of-sllong-max

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

Theorem: sllong-max-bound

(defthm sllong-max-bound
  (>= (sllong-max) 9223372036854775807)
  :rule-classes :linear)

Subtopics

Ushort-max-vs-sllong-max: Relation between unsigned int and signed long long maxima.
Ulong-max-vs-sllong-max: Relation between unsigned long and signed long long maxima.
Uint-max-vs-sllong-max: Relation between unsigned int and signed long long maxima.
Uchar-max-vs-sllong-max: Relation between unsigned int and signed long long maxima.
Slong-max-<=-sllong-max: General relation between signed long and signed long long maxima.
Slong-max-vs-sllong-max: Relation between signed long and signed long long maxima.