diff options
| author | Pierre Roux | 2020-09-03 13:16:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:19 +0100 |
| commit | ec24b26be7795af27256d39431e1c4e3d42fe3b7 (patch) | |
| tree | 6e6e586f0507043994bcc6e59503059201e46f7b /theories/Numbers | |
| parent | 7ea7834b442cbfbf3299536020cb033702b2535c (diff) | |
[numeral notation] Q
Previously rationals were all parsed as a pair numerator, denominator.
This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not
be tell apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.
Now, decimal dot is still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1
= (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are.
A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/DecimalQ.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/HexadecimalQ.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v index d2cd061594..f666c29643 100644 --- a/theories/Numbers/DecimalQ.v +++ b/theories/Numbers/DecimalQ.v @@ -15,7 +15,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q. +Lemma of_to (q:IQ) : forall d, to_decimal q = Some d -> of_decimal d = q. Admitted. (* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *) diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v index ce6f074d70..b773aede8c 100644 --- a/theories/Numbers/HexadecimalQ.v +++ b/theories/Numbers/HexadecimalQ.v @@ -16,7 +16,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ. Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. +Lemma of_to (q:IQ) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. Admitted. (* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *) |