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 name 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 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.
- Nat=>bendian*
- Convert a natural number to
its minimum-length big-endian list of digits.
- Defthm-dab-return-types
- Introduce additional return type theorems for
the conversions from natural numbers to digits.
- Nat=>lendian
- Convert a natural number to
its little-endian list of digits of specified length.
- Lendian=>nat
- Convert a little-endian list of digits to their value.
- Trim-lendian*
- Remove all the most significant zero digits
from a little-endian representation.
- Nat=>bendian
- Convert a natural number to
its big-endian list of digits of specified length.
- Dab-digit-list-fix
- Fixing function for dab-digit-listp.
- Ungroup-bendian
- Ungroup digits from a larger base to a smaller base, little-endian.
- Trim-bendian*
- Remove all the most significant zero digits
from a big-endian representation.
- Group-bendian
- Group digits from a smaller base to a larger base, big-endian.
- Bendian=>nat
- Convert a big-endian list of digits to their value.
- Dab-digit-listp
- Recognize true lists of digits in the specified base.
- Digits=>nat-injectivity-theorems
- Theorems about the injectivity of
the conversions from digits to natural numbers.
- Nat=>lendian+
- Convert a natural number to
its non-empty minimum-length little-endian list of digits.
- Nat=>bendian+
- Convert a natural number to
its non-empty minimum-length big-endian list of digits.
- Dab-basep
- Recognize valid bases for representing natural numbers as digits.
- Trim-lendian+
- Remove all the most significant zero digits
from a little-endian representation,
but leave one zero if all the digits are zero.
- Digits=>nat=>digits-inverses-theorems
- Theorems about converting digits to natural numbers and back.
- 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.
- Nat=>digits-injectivity-theorems
- Theorems about the injectivity of
the conversions from natural numbers to digits.
- Group/ungroup-inverses-theorems
- Theorems about grouping and ungrouping digits.
- Dab-digitp
- Recognize valid digits
for representing natural numbers as digits in the specified base.
- Dab-digit-fix
- Fixing function for dab-digitp.
- 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.
