Showing changes from revision #4 to #5:
Added | Removed | Changed
< decimal numeral representation of the natural numbers
The decimal numeral representations of the natural numbers as familiar from school mathematics.
Let the type of decimal digits, which we shall denote as , be the type inductively generated by the terms , , , , , , , , ,
The type of decimal numeral representations of the natural numbers, which we shall denote as , is a higher inductive type generated by:
A term representing the empty string of digits
A function: representing concatenation of a digit and a string of digits.
A dependent product of identities
representing that adding 0 to the left of any string of digits does not change the underlying value of the decimal numeral representation.
TODO: Define a successor function and show that is equivalent to the natural numbers. Then prove the addition and long multiplication algorithms for decimal numeral representations.
Last revised on June 13, 2022 at 06:21:09. See the history of this page for a list of all contributions to it.