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.
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.