		Search-engine friendly clone of the ACL2 documentation.

Std/strings

Std/strings/digit-to-char

Theorems about the built-in digit-to-char.

Definitions and Theorems

Theorem: digit-to-char-injective

(defthm digit-to-char-injective
        (implies (and (integer-range-p 0 16 x)
                      (integer-range-p 0 16 y))
                 (equal (equal (digit-to-char x)
                               (digit-to-char y))
                        (equal x y))))

Theorem: zero-digit-to-char

(defthm zero-digit-to-char
        (equal (equal (digit-to-char x) #\0)
               (or (not (integerp x))
                   (<= x 0)
                   (< 15 x))))