		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Sshort-min

Minimum ACL2 integer value of type signed short.

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

Definitions and Theorems

Function: sshort-min

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

Theorem: integerp-of-sshort-min

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

Theorem: sshort-min-bound

(defthm sshort-min-bound
  (<= (sshort-min) -32768)
  :rule-classes :linear)

Subtopics

Sshort-min-<=-schar-min: General relation between signed short and signed char minima.
Sshort-min-vs-sint-min: Relation between signed short and signed int minima.
Sint-min-<=-sshort-min: General relation between signed int and signed short minima.
Schar-min-vs-sshort-min: Relation between signed char and signed short minima.