A character set for
Function:
(defun lcletter/digit-chars$inline nil (declare (xargs :guard t)) 10633823807823001954989730196329857024)
Theorem:
(defthm charset-p-of-lcletter/digit-chars (charset-p (lcletter/digit-chars)))
Theorem:
(defthm char-in-charset-p-of-lcletter/digit-chars (equal (char-in-charset-p x (lcletter/digit-chars)) (lcletter/digit-char-p x)))