		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Uint-max

Maximum ACL2 integer value of type unsigned int.

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

Definitions and Theorems

Function: uint-max

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

Theorem: integerp-of-uint-max

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

Theorem: uint-max-bound

(defthm uint-max-bound
  (>= (uint-max) 65535)
  :rule-classes :linear)

Subtopics

Ushort-max-<=-uint-max: General relation between unsigned short and unsigned int maxima.
Ushort-max-vs-uint-max: Relation between unsigned short and unsigned int maxima.
Uint-max-<=-ulong-max: General relation between unsigned int and unsigned long maxima.
Uint-max-vs-ulong-max: Relation between unsigned int and unsigned long maxima.
Uint-max-vs-slong-max: Relation between unsigned int and signed long maxima.
Uint-max-vs-sllong-max: Relation between unsigned int and signed long long maxima.