EXPLODE-NONNEGATIVE-INTEGER.html -- ACL2 Version 2.8

EXPLODE-NONNEGATIVE-INTEGER

the list of characters in the decimal form of a number

Major Section:  PROGRAMMING

Example:
ACL2 !>(explode-nonnegative-integer 325 nil)
(#3 #2 #5)

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

The guard for explode-nonnegative-integer requires the first argument to be a nonnegative integer.