		Search-engine friendly clone of the ACL2 documentation.

Nondigit-chars

A character set for nondigit-char-p.

Function: nondigit-chars$inline

(defun nondigit-chars$inline nil
 (declare (xargs :guard t))
 115792089237316195423570985008687907853269984665640564039457296059011954638847)

Theorem: charset-p-of-nondigit-chars

(defthm charset-p-of-nondigit-chars
  (charset-p (nondigit-chars)))

Theorem: char-in-charset-p-of-nondigit-chars

(defthm char-in-charset-p-of-nondigit-chars
  (equal (char-in-charset-p x (nondigit-chars))
         (nondigit-char-p x)))