		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Char-format-8u

The char format defined by 8 bits and unsignedness.

Signature
(char-format-8u) → format
Returns: format — Type (char-formatp format).

This is the simplest format of char. It is not clear whether it is the most common or not.

Definitions and Theorems

Function: char-format-8u

(defun char-format-8u nil
  (declare (xargs :guard t))
  (let ((__function__ 'char-format-8u))
    (declare (ignorable __function__))
    (make-char-format :signedp nil)))

Theorem: char-formatp-of-char-format-8u

(defthm char-formatp-of-char-format-8u
  (b* ((format (char-format-8u)))
    (char-formatp format))
  :rule-classes :rewrite)

Theorem: char-format->max-of-char-format-8u

(defthm char-format->max-of-char-format-8u
  (equal (char-format->max (char-format-8u)
                           (uchar-format-8)
                           (schar-format-8tcnt))
         255))

Theorem: char-format->min-of-char-format-8u

(defthm char-format->min-of-char-format-8u
  (equal (char-format->min (char-format-8u)
                           (uchar-format-8)
                           (schar-format-8tcnt))
         0))