		Search-engine friendly clone of the ACL2 documentation.

Digit-to-char

Map a digit to a character

Example:
ACL2 !>(digit-to-char 8)
#\8

For an integer n from 0 to 15, (digit-to-char n) is the character corresponding to n in hex notation, using uppercase letters for digits exceeding 9. If n is 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.

Function: digit-to-char

(defun digit-to-char (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n) (<= n 15))))
  (case n
    (1 #\1)
    (2 #\2)
    (3 #\3)
    (4 #\4)
    (5 #\5)
    (6 #\6)
    (7 #\7)
    (8 #\8)
    (9 #\9)
    (10 #\A)
    (11 #\B)
    (12 #\C)
    (13 #\D)
    (14 #\E)
    (15 #\F)
    (otherwise #\0)))