		Search-engine friendly clone of the ACL2 documentation.

Code-char-inverses-theorems

code-char and char-code are mutual inverses.

Theorem: char-code-of-code-char

(defthm char-code-of-code-char
  (equal (char-code (code-char code))
         (unsigned-byte-fix 8 code)))

Theorem: code-char-of-char-code

(defthm code-char-of-char-code
  (equal (code-char (char-code char))
         (char-fix char)))