digit-to-char

(in-package "ACL2")

(defsection std/strings/digit-to-char
  :parents (std/strings)
  :short "Theorems about the built-in @(tsee digit-to-char)."
  (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)))
    :hints (("Goal" :in-theory (enable digit-to-char))))
  (defthmd zero-digit-to-char
    (equal (equal (digit-to-char x) #\0)
      (or (not (integerp x)) (<= x 0) (< 15 x)))
    :hints (("Goal" :in-theory (enable digit-to-char)))))