Digits-any-base
Conversions between natural numbers
and their representations as digits in arbitrary bases.
In these utilities, the digits are natural numbers below the base.
The base (a natural number above 1) is supplied as argument.
There are conversions for big-endian and little-endian representations.
There are conversions to represent natural numbers as lists of digits
of fixed length, of minimum length, and of minimum non-zero length.
The names of some functions in these utilities start with dab,
which stands for `digits any base'.
Without this prefix, the names seem too ``general''.
Subtopics
- Defdigits
- Generate specialized versions of the operations to convert between natural numbers and digits, using specified existing recognizers and fixers for the digits.
- Nat=>lendian*
- Convert a natural number to
its minimum-length little-endian list of digits.
- Group-lendian
- Group digits from a smaller base to a larger base, little-endian.
- Defdigit-grouping
- Generate specialized versions of the operations to group and ungroup digits in arbitrary bases, based on existing instances of defdigits.
- Ungroup-lendian
- Ungroup digits from a larger base to a smaller base, little-endian.
- Lendian=>nat
- Convert a little-endian list of digits to their value.
- Defthm-dab-return-types
- Introduce additional return type theorems for
the conversions from natural numbers to digits.
- Bendian=>nat
- Convert a big-endian list of digits to their value.
- Nat=>bendian*
- Convert a natural number to
its minimum-length big-endian list of digits.
- Trim-bendian*
- Remove all the most significant zero digits
from a big-endian representation.
- Trim-lendian*
- Remove all the most significant zero digits
from a little-endian representation.
- Nat=>lendian
- Convert a natural number to
its little-endian list of digits of specified length.
- Dab-digit-list-fix
- Fixing function for dab-digit-listp.
- Nat=>bendian
- Convert a natural number to
its big-endian list of digits of specified length.
- Ungroup-bendian
- Ungroup digits from a larger base to a smaller base, little-endian.
- Group-bendian
- Group digits from a smaller base to a larger base, big-endian.
- Digits=>nat-injectivity-theorems
- Theorems about the injectivity of
the conversions from digits to natural numbers.
- Dab-digit-listp
- Recognize true lists of digits in the specified base.
- Nat=>lendian+
- Convert a natural number to
its non-empty minimum-length little-endian list of digits.
- Dab-basep
- Recognize valid bases for representing natural numbers as digits.
- Nat=>bendian+
- Convert a natural number to
its non-empty minimum-length big-endian list of digits.
- Digits=>nat=>digits-inverses-theorems
- Theorems about converting digits to natural numbers and back.
- Trim-lendian+
- Remove all the most significant zero digits
from a little-endian representation,
but leave one zero if all the digits are zero.
- Trim-bendian+
- Remove all the most significant zero digits
from a big-endian representation,
but leave one zero if all the digits are zero.
- Nat=>digits=>nat-inverses-theorems
- Theorems about converting natural numbers to digits and back.
- Dab-digitp
- Recognize valid digits
for representing natural numbers as digits in the specified base.
- Group/ungroup-inverses-theorems
- Theorems about grouping and ungrouping digits.
- Dab-digit-fix
- Fixing function for dab-digitp.
- Nat=>digits-injectivity-theorems
- Theorems about the injectivity of
the conversions from natural numbers to digits.
- Dab-base
- Fixtype for dab-basep.
- Digits-any-base-pow2
- Conversions between natural numbers
and their representations as digits in power-of-two bases.
- Dab-base-fix
- Fixing function for dab-basep.
