		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Schar-format-8tcnt

The signed char format defined by 8 bits, two's complement, and no trap representations.

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

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

Definitions and Theorems

Function: schar-format-8tcnt

(defun schar-format-8tcnt nil
  (declare (xargs :guard t))
  (let ((__function__ 'schar-format-8tcnt))
    (declare (ignorable __function__))
    (make-schar-format :signed (signed-format-twos-complement)
                       :trap nil)))

Theorem: schar-formatp-of-schar-format-8tcnt

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

Theorem: schar-format->max-of-schar-format-8tcnt

(defthm schar-format->max-of-schar-format-8tcnt
  (equal (schar-format->max (schar-format-8tcnt)
                            (uchar-format-8))
         127))

Theorem: schar-format->min-of-schar-format-8tcnt

(defthm schar-format->min-of-schar-format-8tcnt
  (equal (schar-format->min (schar-format-8tcnt)
                            (uchar-format-8))
         -128))