		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Uchar-max

Maximum ACL2 integer value of type unsigned char.

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

Definitions and Theorems

Function: uchar-max

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

Theorem: integerp-of-uchar-max

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

Theorem: uchar-max-bound

(defthm uchar-max-bound
  (>= (uchar-max) 255)
  :rule-classes :linear)

Subtopics

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