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