diff options
| author | Pierre Roux | 2018-10-14 15:33:31 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:29 +0200 |
| commit | 49c5de7ead9d008d91a63316e6037bcc9c1f1d52 (patch) | |
| tree | dea3c2b04374888bfbdd802742df4199656ae83e /test-suite | |
| parent | 7e1243a174e28535d9b35b558ed94f1548acd78c (diff) | |
Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/micromega/square.v | 2 | ||||
| -rw-r--r-- | test-suite/success/QArithSyntax.v | 9 |
2 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 7266b662fa..9efb81a901 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -54,7 +54,7 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). diff --git a/test-suite/success/QArithSyntax.v b/test-suite/success/QArithSyntax.v new file mode 100644 index 0000000000..2f2ee0134a --- /dev/null +++ b/test-suite/success/QArithSyntax.v @@ -0,0 +1,9 @@ +Require Import QArith. +Open Scope Q_scope. +Check (eq_refl : 1.02 = 102 # 100). +Check (eq_refl : 1.02e1 = 102 # 10). +Check (eq_refl : 1.02e+03 = 1020). +Check (eq_refl : 1.02e+02 = 102 # 1). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = -1 # 10000). +Check (eq_refl : -0.50 = - 50 # 100). |