diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 09:34:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 09:37:53 +0200 |
| commit | d17237cfd3a67b9a93de98a23ae29869456d2028 (patch) | |
| tree | 5a323cfed9cee00a8dc23b1fac710bbe408c23aa /test-suite | |
| parent | 91f44b164c5d9fa170a8faa7227aff08c1335861 (diff) | |
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.out | 11 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 9 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index b3d2580ac..823418cc1 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -6,3 +6,14 @@ : nat * nat * (nat * nat) pair (pair O (S (S O))) (pair (S (S O)) O) : prod (prod nat nat) (prod nat nat) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (2, (2, 0))) + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (0, (2, 4))) + : nat * nat * nat * (nat * (nat * nat)) +pair (pair (pair O (S (S O))) (S (S (S (S O))))) + (pair (S (S (S (S O)))) (pair (S (S O)) O)) + : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 32d70ac18..f37772534 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -10,3 +10,12 @@ Check ((0,2),(2,2)). Unset Printing Notations. Check [<0,2>]. Set Printing Notations. + +Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)). +Check <<0,2,4>>. +Check (((0,2),4),(4,(2,0))). +Check (((0,2),4),(2,(2,0))). +Check (((0,2),4),(0,(2,4))). +Unset Printing Notations. +Check <<0,2,4>>. +Set Printing Notations. |