diff options
| author | Hugo Herbelin | 2020-03-17 13:00:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 5d1c4ae7b8931c7a1dec5f61c2571919319aeb4a (patch) | |
| tree | cca84c8a59556b3ddbd27e74e3d0917e4847ba18 | |
| parent | f7687371270e0b3fd3b61db3f25128c567aa7033 (diff) | |
Testing notations which are specific numerals.
| -rw-r--r-- | test-suite/output/NumeralNotations.out | 12 | ||||
| -rw-r--r-- | test-suite/output/NumeralNotations.v | 23 |
2 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index bb299eff97..060877707b 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -222,3 +222,15 @@ let v : ty := Build_ty Type type in v : ty : nat (-1000)%Z : Z +0 + : Prop ++0 + : bool +-0 + : bool +00 + : nat * nat +1000 + : Prop +1_000 + : list nat diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 31154d9f45..47e1b127cb 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -464,3 +464,26 @@ Module Test21. Check (-1_000)%Z. End Test21. + +Module Test22. + +Notation "0" := False. +Notation "+0" := true. +Notation "-0" := false. +Notation "00" := (0%nat, 0%nat). +Check 0. +Check +0. +Check -0. +Check 00. + +Notation "1000" := True. +Notation "1_000" := (cons 1 nil). +Check 1000. +Check 1_000. + +(* To do: preserve parsing of -0: +Require Import ZArith. +Check (-0)%Z. +*) + +End Test22. |