		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Schar-min

Minimum ACL2 integer value of type signed char.

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

Definitions and Theorems

Function: schar-min

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

Theorem: integerp-of-schar-min

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

Theorem: schar-min-bound

(defthm schar-min-bound
  (<= (schar-min) -128)
  :rule-classes :linear)

Subtopics

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