		Search-engine friendly clone of the ACL2 documentation.

Char-bit-constrp

Constraints on the value of CHAR_BIT.

It must be an integer that is at least 8.

Function: char-bit-constrp

(defun char-bit-constrp (char-bit)
  (declare (xargs :guard t))
  (and (integerp char-bit)
       (>= char-bit 8)))

Theorem: booleanp-of-char-bit-constrp

(defthm booleanp-of-char-bit-constrp
  (b* ((yes/no (char-bit-constrp char-bit)))
    (booleanp yes/no))
  :rule-classes :rewrite)