		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Schar-max

Maximum ACL2 integer value of type signed char.

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

Definitions and Theorems

Function: schar-max

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

Theorem: integerp-of-schar-max

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

Theorem: schar-max-bound

(defthm schar-max-bound
  (>= (schar-max) 127)
  :rule-classes :linear)

Subtopics

Schar-max-<=-sshort-max: General relation between signed char and signed short maxima.
Schar-max-vs-sshort-max: Relation between signed char and signed short maxima.