		Search-engine friendly clone of the ACL2 documentation.

Schar-max

Maximum mathematical integer value of type signed char.

Given the assumptions explained in ienv, this is +127.

We keep this nullary function closed for more abstraction.

Function: schar-max

(defun schar-max nil
  (declare (xargs :guard t))
  (let ((__function__ 'schar-max))
    (declare (ignorable __function__))
    127))

Theorem: natp-of-schar-max

(defthm natp-of-schar-max
  (b* ((val (schar-max))) (natp val))
  :rule-classes :rewrite)