		Search-engine friendly clone of the ACL2 documentation.

Bool-formats

Bool-format-lsb

The _Bool format defined by a single byte with its least significant bit as the value bit, and no trap representations.

Signature
(bool-format-lsb) → format
Returns: format — Type (bool-formatp format).

Definitions and Theorems

Function: bool-format-lsb

(defun bool-format-lsb nil
  (declare (xargs :guard t))
  (make-bool-format :byte-size 1
                    :value-index 0
                    :trap nil))

Theorem: bool-formatp-of-bool-format-lsb

(defthm bool-formatp-of-bool-format-lsb
  (b* ((format (bool-format-lsb)))
    (bool-formatp format))
  :rule-classes :rewrite)

Theorem: bool-format-wfp-of-bool-format-lsb

(defthm bool-format-wfp-of-bool-format-lsb
  (bool-format-wfp (bool-format-lsb)
                   uchar-format))