		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Ulong-max

Maximum ACL2 integer value of type unsigned long.

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

Definitions and Theorems

Function: ulong-max

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

Theorem: integerp-of-ulong-max

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

Theorem: ulong-max-bound

(defthm ulong-max-bound
  (>= (ulong-max) 4294967295)
  :rule-classes :linear)

Subtopics

Ulong-max-<=-ullong-max: General relation between unsigned long and unsigned long long maxima.
Ulong-max-vs-ullong-max: Relation between unsigned long and unsigned long long maxima.
Ulong-max-vs-sllong-max: Relation between unsigned long and signed long long 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.