diff options
Diffstat (limited to 'test-suite/output/RealSyntax.v')
| -rw-r--r-- | test-suite/output/RealSyntax.v | 44 |
1 files changed, 37 insertions, 7 deletions
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 69ce3ef5f9..790d5c654f 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -8,18 +8,48 @@ Check 1_.5_e1_%R. 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 1.02e1. +Check IZR 102 / IZR (Z.pow_pos 10 1). +Check 1.02e+03. +Check IZR 102 * IZR (Z.pow_pos 10 1). +Check 1.02e+02. +Check IZR 102. +Check 10.2e-1. +Check 1.02. Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). Check (eq_refl : -0x1a = - 26). Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)). Check (eq_refl : -0x1ae2 = -6882). -Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)). -Check (eq_refl : 0xb.2cp8 = 2860). -Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)). +Check 0xb.2cp2. +Check IZR 2860 / IZR (Z.pow_pos 2 6). +Check 0xb.2cp8. +Check 2860. +Check -0xb.2cp-2. +Check - (IZR 2860 / IZR (Z.pow_pos 2 10)). +Check 0. +Check 000. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0.0012. +Check 42e3. +Check 42e-3. + +Open Scope hex_R_scope. + +Check 0x0. +Check 0x000. +Check 42. +Check 0x2a. +Check 1.23. +Check 0x1.23. +Check 0x0.0012. +Check 0x2ap3. +Check 0x2ap-3. + +Close Scope hex_R_scope. Require Import Reals. |