		Search-engine friendly clone of the ACL2 documentation.

Letter/digit-chars

A character set for letter/digit-char-p.

Function: letter/digit-chars$inline

(defun letter/digit-chars$inline nil
  (declare (xargs :guard t))
  10633823810298881996667002598709002240)

Theorem: charset-p-of-letter/digit-chars

(defthm charset-p-of-letter/digit-chars
  (charset-p (letter/digit-chars)))

Theorem: char-in-charset-p-of-letter/digit-chars

(defthm char-in-charset-p-of-letter/digit-chars
  (equal (char-in-charset-p x (letter/digit-chars))
         (letter/digit-char-p x)))