		Search-engine friendly clone of the ACL2 documentation.

Decimal-digits-std/strings-theorems

Theorems about Java decimal digits and functions in Std/strings.

Theorem: dec-digitp-of-char-code

(defthm dec-digitp-of-char-code
  (equal (dec-digitp (char-code char))
         (str::dec-digit-char-p char)))

Theorem: dec-digit-listp-of-chars=>nats

(defthm dec-digit-listp-of-chars=>nats
  (equal (dec-digit-listp (chars=>nats chars))
         (str::dec-digit-char-list*p chars)))