		Search-engine friendly clone of the ACL2 documentation.

Numbers

Decimal

Functions for working with decimal (base 10) numbers in strings.

Subtopics

Parse-nat-from-string: Parse a natural number from a string, at some offset.
Parse-nat-from-charlist: Parse a natural number from the beginning of a character list.
Nat-to-dec-chars: Convert a natural number into a list of characters.
Dec-digit-chars-value: Coerces a dec-digit-char-list*p into a natural number.
Dec-digit-char-p: Recognizer for numeric characters (0-9).
Dec-digit-char-listp: Recognize lists of decimal digit characters.
Take-leading-dec-digit-chars: Collect any leading digits from the start of a character list.
Dec-digit-char-value: Coerces a dec-digit-char-p character into a number.
Dec-digit-char-list*p: Recognizes lists of dec-digit-char-p characters.
Nat-to-dec-string-width: Convert a natural number into a string with the given width.
Nat-to-dec-string: Convert a natural number into a string with its digits.
Dec-digit-string-p: Recognizer for strings whose characters are all decimal digits.
Strval: Interpret a string as a decimal number.
Skip-leading-digits: Skip over any leading digits at the start of a character list.
Nat-to-dec-string-size: Number of characters in the decimal representation of a natural.
Int-to-dec-string-width: Convert an integer into a string with a fixed number of digits.
Int-to-dec-string: Convert an integer into a string with its digits.
Nonzero-dec-digit-char-p: Recognizer for non-zero numeric characters (1-9).
Nat-to-dec-string-list: Convert a list of natural numbers into a list of strings.
Int-to-dec-string-list: Convert a list of integers into a list of strings.
Revappend-nat-to-dec-chars: More efficient version of (revappend (nat-to-dec-chars n) acc).