diff options
| author | Hugo Herbelin | 2016-07-17 09:22:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 10:45:27 +0200 |
| commit | 152aca663d76f0cfda21ddef880050f21bfe4995 (patch) | |
| tree | 7d2bf7549f1e068aa38b4ecfd80c8677936cd0ab /test-suite | |
| parent | d17237cfd3a67b9a93de98a23ae29869456d2028 (diff) | |
Fixing a bug in recognizing a recursive pattern of notations
immediately in the scope of another recursive pattern.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 13 |
2 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 823418cc15..8b3fa31618 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -17,3 +17,11 @@ pair (pair O (S (S O))) (pair (S (S O)) O) 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)) +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +fun x y : nat => Nat.add x y + : forall (_ : nat) (_ : nat), nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index f377725348..d791042043 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -19,3 +19,16 @@ Check (((0,2),4),(0,(2,4))). Unset Printing Notations. Check <<0,2,4>>. Set Printing Notations. + +(**********************************************************************) +(* Check notations with recursive notations both in binders and terms *) + +Notation "'ETA' x .. y , f" := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder). +Check ETA (x:nat) (y:nat), Nat.add. +Check ETA (x y:nat), Nat.add. +Check ETA x y, Nat.add. +Unset Printing Notations. +Check ETA (x:nat) (y:nat), Nat.add. +Set Printing Notations. |