diff options
author | 2017-06-26 18:40:11 +0200 | |
---|---|---|
committer | 2017-07-26 15:03:31 +0200 | |
commit | ada7875e95cba2f08902c55cfd3f69d6cc80cac3 (patch) | |
tree | f989fe34a04bfc803f5bd6449a198bd9558ee116 /test-suite | |
parent | 51d418636adf30bcf4e37a5b7b479a7d54dbedb2 (diff) |
Adding support for recursive notations of the form "x , .. , y , z".
Since camlp5 parses from left, the last ", z" was parsed as part of an
arbitrary long list of "x1 , .. , xn" and a syntax error was raised
since an extra ", z" was still expected.
We support this by translating "x , .. , y , z" into "x , y , .. , z"
and reassembling the arguments appropriately after parsing.
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}. |