diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations2.out | 24 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 29 |
2 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 5541ccf57b..ad60aeccce 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -60,3 +60,27 @@ exist (Q x) y conj : nat -> nat {1, 2} : nat -> Prop +a# + : Set +a# + : Set +a≡ + : Set +a≡ + : Set +.≡ + : Set +.≡ + : Set +.a# + : Set +.a# + : Set +.a≡ + : Set +.a≡ + : Set +.α + : Set +.α + : Set diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 1d8278c088..ceb29d1b9e 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -116,3 +116,32 @@ Check %j. Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))). Check ({1, 2}). + +(**********************************************************************) +(* Check notations of the form ".a", ".a≡", "a≡" *) +(* Only "a#", "a≡" and ".≡" were working properly for parsing. The *) +(* other ones were working only for printing. *) + +Notation "a#" := nat. +Check nat. +Check a#. + +Notation "a≡" := nat. +Check nat. +Check a≡. + +Notation ".≡" := nat. +Check nat. +Check .≡. + +Notation ".a#" := nat. +Check nat. +Check .a#. + +Notation ".a≡" := nat. +Check nat. +Check .a≡. + +Notation ".α" := nat. +Check nat. +Check .α. |