		Search-engine friendly clone of the ACL2 documentation.

Explode-nonnegative-integer

The list of characters in the radix-r form of a number

Examples:
ACL2 !>(explode-nonnegative-integer 925 10 nil)
(#9 #2 #5)
ACL2 !>(explode-nonnegative-integer 325 16 nil)
(#3 #9 #D)

For a non-negative integer n, (explode-nonnegative-integer n r nil) is the list of characters in the radix-r (base-r) representation of n.

The guard for explode-nonnegative-integer requires the first argument to be a nonnegative integer and second argument to be a valid radix for ACL2 (2, 8, 10, or 16).

Function: explode-nonnegative-integer

(defun explode-nonnegative-integer (n print-base ans)
  (declare (xargs :guard (and (integerp n)
                              (>= n 0)
                              (print-base-p print-base))))
  (cond ((or (zp n)
             (not (print-base-p print-base)))
         (cond ((null ans) '(#\0)) (t ans)))
        (t (explode-nonnegative-integer
                (floor n print-base)
                print-base
                (cons (digit-to-char (mod n print-base))
                      ans)))))