Showing changes from revision #2 to #3:
Added | Removed | Changed
Idea
The decimal numbers as familiar from school mathematics.
Contents
Definition
The type of decimal numbers, denoted , has is several defined definitions as a thehigher inductive type . generated by:
Definition 1
Decimal numbers are defined as the higher inductive type generated by:
Raw ring structure on the decimal numbers
- A function
- A dependent product of functions between identities representing that equivalent decimals are equal:
- A set-truncator
Zero
We define zero to be the following:
Addition
We define addition to be the following:
for , , , .
Negation
We define negation to be the following:
for , .
Subtraction
We define subtraction to be the following:
for , , , .
One
We define one to be the following:
Multiplication
We define multiplication to be the following:
for , , , .
Exponentiation
We define exponentiation to be the following:
for , , .
Properties
TODO: Show that the decimal numbers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are a Heyting integral subdomain of the rational numbers.
10 is a unit term.
Thus this is true:
this forms the basis of scientific notation.
See also