Major Section: ACL2-BUILT-INS
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 15, inclusive.
To see the ACL2 definition of this function, see pf.