		Search-engine friendly clone of the ACL2 documentation.

Code-char

Code-char-lemmas

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

Definitions and Theorems

Theorem: default-code-char

(defthm default-code-char
  (implies (or (zp x) (not (< x 256)))
           (equal (code-char x) (code-char 0))))

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

(defthm equal-of-code-char-and-code-char
  (equal (equal (code-char x) (code-char y))
         (let ((zero-x (or (zp x) (>= x 256)))
               (zero-y (or (zp y) (>= y 256))))
           (if zero-x zero-y (equal x y)))))

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

(defthm equal-of-code-code-and-constant
  (implies (syntaxp (quotep c))
           (equal (equal (code-char x) c)
                  (and (characterp c)
                       (if (equal c (code-char 0))
                           (or (zp x) (not (< x 256)))
                         (equal x (char-code c)))))))