		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uchar-format-8

The unsigned char format defined by 8 bits.

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

This is the simplest and most common format for unsigned char.

Definitions and Theorems

Function: uchar-format-8

(defun uchar-format-8 nil
  (declare (xargs :guard t))
  (let ((__function__ 'uchar-format-8))
    (declare (ignorable __function__))
    (make-uchar-format :size 8)))

Theorem: uchar-formatp-of-uchar-format-8

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

Theorem: uchar-format->max-of-uchar-format-8

(defthm uchar-format->max-of-uchar-format-8
  (equal (uchar-format->max (uchar-format-8))
         255))