diff options
| author | Pierre Roux | 2020-09-03 13:19:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:19 +0100 |
| commit | b6c13afd432ce1957315e94c1ce8c06aa848fe5a (patch) | |
| tree | 63110d324a51f65436d7c7e01abd6872029c2491 /plugins/syntax/dune | |
| parent | 11f8d8fca374565b4cad542e131fd32a50a70440 (diff) | |
[numeral notation] R
Previously real constants were parsed by an unproved OCaml code. The
parser and printer are now implemented in Coq, which will enable a
proof and hopefully make it easier to maintain / make evolve.
Previously reals were all parsed as an integer, an integer multiplied
by a power of ten or an integer divided by a power of ten. 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 parsed as a rational and exponents are parsed as a
product or division by a power of ten. For instance, 1.02 is parsed as
Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos
10 2).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R
(102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
Diffstat (limited to 'plugins/syntax/dune')
| -rw-r--r-- | plugins/syntax/dune | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/plugins/syntax/dune b/plugins/syntax/dune index b395695c8a..1b3d7598da 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -13,13 +13,6 @@ (libraries coq.vernac)) (library - (name r_syntax_plugin) - (public_name coq.plugins.r_syntax) - (synopsis "Coq syntax plugin: reals") - (modules r_syntax) - (libraries coq.vernac)) - -(library (name int63_syntax_plugin) (public_name coq.plugins.int63_syntax) (synopsis "Coq syntax plugin: int63") |