diff options
| author | Pierre Roux | 2018-10-13 22:17:27 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:25 +0200 |
| commit | 7e1243a174e28535d9b35b558ed94f1548acd78c (patch) | |
| tree | 3f4176549aa679f99e7d9dd71397b1cf0daa2279 /test-suite | |
| parent | 552bb5aba750785d8f19aa7b333baa59e9199369 (diff) | |
Make R parser parse decimals (e.g., 1.02e+01)
RealField.v is slightly modified so that the ring/field tactics
consider the term (IZR (Z.pow_pos 10 _)) produced when parsing
exponents as constants.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/RealSyntax.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v new file mode 100644 index 0000000000..2765200991 --- /dev/null +++ b/test-suite/success/RealSyntax.v @@ -0,0 +1,19 @@ +Require Import Reals. +Open Scope R_scope. +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+02 = IZR 102). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). +Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)). + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. |