Major Section: PROGRAMMING Example: ACL2 !>(digit-to-char 8)
#\8For an integer nfrom 0 to 15, (digit-to-char n)is the
character corresponding to nin hex notation, using uppercase
letters for digits exceeding 9. If nis in the appropriate range,
that result is of course also the binary, octal, and decimal
digit. The guard for digit-to-char requires its argument to be
an integer between 0 and 9, inclusive.