		Search-engine friendly clone of the ACL2 documentation.

Number-char-p

Recognize digits 0-9.

Function: number-char-p

(defun number-char-p (x)
  (declare (xargs :guard t))
  (and (characterp x)
       (str::dec-digit-char-p x)))

Theorem: booleanp-of-number-char-p

(defthm booleanp-of-number-char-p
  (booleanp (number-char-p x))
  :rule-classes :type-prescription)

Theorem: characterp-when-number-char-p

(defthm characterp-when-number-char-p
  (implies (number-char-p x)
           (characterp x))
  :rule-classes :compound-recognizer)

Number-charlist-p: (number-charlist-p x) recognizes lists where every element satisfies number-char-p.
Number-chars: A character set for number-char-p.