		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))))