		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Sshort-max

Maximum ACL2 integer value of type signed short.

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

Definitions and Theorems

Function: sshort-max

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

Theorem: integerp-of-sshort-max

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

Theorem: sshort-max-bound

(defthm sshort-max-bound
  (>= (sshort-max) 32767)
  :rule-classes :linear)

Subtopics

Sshort-max-<=-sint-max: General relation between signed short and signed int maxima.
Sshort-max-vs-sint-max: Relation between signed short and signed int maxima.
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.