		Search-engine friendly clone of the ACL2 documentation.

Bytes

Char-bit

Parameter for the specific value of CHAR_BIT.

This constrained nullary function is a parameter of our C formalization. It expresses the value of CHAR_BIT.

Definition: char-bit

(encapsulate (((char-bit) => *))
  (acl2::record-expansion (local (define char-bit nil 8))
                          (local (value-triple :elided)))
  (defrule char-bit-constrp-of-char-bit
    (char-bit-constrp (char-bit))))

Definitions and Theorems

Theorem: char-bit-constrp-of-char-bit

(defthm char-bit-constrp-of-char-bit
  (char-bit-constrp (char-bit)))

Theorem: posp-of-char-bit

(defthm posp-of-char-bit
  (posp (char-bit))
  :rule-classes :type-prescription)

Theorem: char-bit-gteq-8

(defthm char-bit-gteq-8
  (>= (char-bit) 8)
  :rule-classes :linear)