diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:25 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:25 +0200 |
commit | 6c179759a5c117b24abe5466ee860f1f7fb29dac (patch) | |
tree | dd15e6023c925db50541107fe1487307dd2d1039 /test-suite | |
parent | 662d6581c852496d5bb62e27893810e2514cdfbb (diff) | |
parent | ada7875e95cba2f08902c55cfd3f69d6cc80cac3 (diff) |
Merge PR #834: Adding support for recursive notations of the form "x , .. , y , z".
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/Notations3.out | 6 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 8 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index ffea0819a..a9ae74fd6 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -109,3 +109,9 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) +{0, 1} + : nat * nat +{0, 1, 2} + : nat * (nat * nat) +{0, 1, 2, 3} + : nat * (nat * (nat * nat)) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 250aecafd..dee0f70f7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -160,3 +160,11 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). + +(**********************************************************************) +(* Test recursive notations with the recursive pattern repeated on the right *) + +Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). +Check {0,1}. +Check {0,1,2}. +Check {0,1,2,3}. |