		Search-engine friendly clone of the ACL2 documentation.

Char-bits

Size of signed, unsigned, and plain char values, in bits.

Function: char-bits

(defun char-bits nil
  (declare (xargs :guard t))
  (let ((__function__ 'char-bits))
    (declare (ignorable __function__))
    8))

Theorem: posp-of-char-bits

(defthm posp-of-char-bits
  (b* ((char-bits (char-bits)))
    (posp char-bits))
  :rule-classes :type-prescription)

Theorem: char-bits-bound

(defthm char-bits-bound
  (b* ((?char-bits (char-bits)))
    (>= char-bits 8))
  :rule-classes :linear)