		Search-engine friendly clone of the ACL2 documentation.

Uchar-max

Maximum mathematical integer value of type unsigned char.

Given the assumptions explained in ienv, this is 255.

Note that the minimum unsigned char is just 0, so there is no need to introduce a function for it.

We keep this nullary function closed for more abstraction.

Function: uchar-max

(defun uchar-max nil
  (declare (xargs :guard t))
  (let ((__function__ 'uchar-max))
    (declare (ignorable __function__))
    255))

Theorem: natp-of-uchar-max

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