		Search-engine friendly clone of the ACL2 documentation.

Char-code

Char-code-lemmas

Lemmas about char-code from the std/strings library.

Definitions and Theorems

Theorem: equal-of-char-code-and-constant

(defthm equal-of-char-code-and-constant
  (implies (syntaxp (quotep c))
           (equal (equal (char-code x) c)
                  (if (characterp x)
                      (and (natp c)
                           (<= c 255)
                           (equal x (code-char c)))
                    (equal c 0)))))

Theorem: equal-of-char-codes

(defthm equal-of-char-codes
  (equal (equal (char-code x) (char-code y))
         (equal (char-fix x) (char-fix y))))