the number, if any, corresponding to a given character
Major Section:  PROGRAMMING

(digit-char-p ch) is the integer corresponding to the character ch in base 10. For example, (digit-char-p #\3) is equal to the integer 3. More generally, an optional second argument specifies the radix (default 10, as indicated above).

The guard for digit-char-p (more precisely, for the function our-digit-char-p that calls of this macro expand to) requires its second argument to be an integer between 2 and 36, inclusive, and its first argument to be a character.

Digit-char-p is a Common Lisp function, though it is implemented in the ACL2 logic as an ACL2 macro. See any Common Lisp documentation for more information.