diff options
| author | coqbot-app[bot] | 2020-11-05 15:32:31 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-05 15:32:31 +0000 |
| commit | afc828b3e207dd39c59d1501d570a88b2012fd2c (patch) | |
| tree | f9af32a8b25439a9eb6c8407f99ad94f78a64fda /test-suite/output/RealSyntax.out | |
| parent | b95c38d3d28a59da7ff7474ece0cb42623497b7d (diff) | |
| parent | e6f7517be65e9f5d2127a86e2213eb717d37e43f (diff) | |
Merge PR #12218: Numeral notations for non inductive types
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
Diffstat (limited to 'test-suite/output/RealSyntax.out')
| -rw-r--r-- | test-suite/output/RealSyntax.out | 101 |
1 files changed, 74 insertions, 27 deletions
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index a9386b2781..a7b7dabb20 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -4,34 +4,81 @@ : R 1.5%R : R -15%R - : R -eq_refl : 1.02 = 1.02 - : 1.02 = 1.02 -eq_refl : 10.2 = 10.2 - : 10.2 = 10.2 -eq_refl : 102e1 = 102e1 - : 102e1 = 102e1 -eq_refl : 102 = 102 - : 102 = 102 -eq_refl : 1.02 = 1.02 - : 1.02 = 1.02 -eq_refl : -1e-4 = -1e-4 - : -1e-4 = -1e-4 -eq_refl : -0.50 = -0.50 - : -0.50 = -0.50 +1.5e1%R + : R +eq_refl : 1.02 = 102e-2 + : 1.02 = 102e-2 +1.02e1 + : R +102e-1 + : R +1.02e3 + : R +102e1 + : R +1.02e2 + : R +102 + : R +10.2e-1 + : R +1.02 + : R +eq_refl : -0.0001 = -1e-4 + : -0.0001 = -1e-4 +eq_refl : -0.50 = -50e-2 + : -0.50 = -50e-2 eq_refl : -26 = -26 : -26 = -26 -eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) - : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) +eq_refl : 0xb.2c%xR = 0xb2cp-8%xR + : 0xb.2c%xR = 0xb2cp-8%xR eq_refl : -6882 = -6882 : -6882 = -6882 -eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) - : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) -eq_refl : 2860 = 2860 - : 2860 = 2860 -eq_refl -: --2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10) - : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - - (2860) / IZR (Z.pow_pos 2 10) +0xb.2cp2%xR + : R +0xb2cp-6%xR + : R +0xb.2cp8%xR + : R +2860 + : R +(-0xb.2cp-2)%xR + : R +- 0xb2cp-10%xR + : R +0 + : R +0 + : R +42 + : R +42 + : R +1.23 + : R +0x1.23%xR + : R +0.0012 + : R +42e3 + : R +42e-3 + : R +0x0 + : R +0x0 + : R +0x2a + : R +0x2a + : R +1.23%R + : R +0x1.23 + : R +0x0.0012 + : R +0x2ap3 + : R +0x2ap-3 + : R |