		Search-engine friendly clone of the ACL2 documentation.

Hex-digit-char-theorems

Some theorems about the library functions str::hex-digit-char-value and str::hex-digit-to-char.

Definitions and Theorems

Theorem: hex-digit-char-value-of-hex-digit-to-char

(defthm
  str::hex-digit-char-value-of-hex-digit-to-char
  (implies
       (integer-range-p 0 16 n)
       (equal (str::hex-digit-char-value (str::hex-digit-to-char n))
              n)))

Theorem: hex-digit-to-char-of-hex-digit-char-value

(defthm
 str::hex-digit-to-char-of-hex-digit-char-value
 (implies
    (str::hex-digit-char-p char)
    (equal (str::hex-digit-to-char (str::hex-digit-char-value char))
           (str::upcase-char char))))