		Search-engine friendly clone of the ACL2 documentation.

Schar-min

Minimum mathematical integer value of type signed char.

Given the assumptions explained in ienv, this is @'-128').

We keep this nullary function closed for more abstraction.

Function: schar-min

(defun schar-min nil
  (declare (xargs :guard t))
  (let ((__function__ 'schar-min))
    (declare (ignorable __function__))
    -128))

Theorem: integerp-of-schar-min

(defthm integerp-of-schar-min
  (b* ((val (schar-min))) (integerp val))
  :rule-classes :rewrite)