diff options
Diffstat (limited to 'test-suite/success/Notations.v')
-rw-r--r-- | test-suite/success/Notations.v | 46 |
1 files changed, 44 insertions, 2 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 661a8757..2371d32c 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -17,10 +17,12 @@ Check (nat |= nat --> nat). (* Check that first non empty definition at an empty level can be of any associativity *) -Definition marker := O. +Module Type v1. Notation "x +1" := (S x) (at level 8, left associativity). -Reset marker. +End v1. +Module Type v2. Notation "x +1" := (S x) (at level 8, right associativity). +End v2. (* Check that empty levels (here 8 and 2 in pattern) are added in the right order *) @@ -59,3 +61,43 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. + +(* Check well-scoping of alpha-renaming of private binders *) +(* see bug #2248 (thanks to Marc Lasson) *) + +Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P). +Check (fun p => {q,r| q + r = p}). + +(* Check that declarations of empty levels are correctly backtracked *) + +Section B. +Notation "*" := 5 (at level 0) : nat_scope. +Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope. +End B. + +(* Should succeed *) +Definition n := 5 * 5. + +(* Check that lonely notations (here FOO) do not modify the visibility + of scoped interpretations (bug #2634 fixed in r14819) *) + +Notation "x ++++ y" := (mult x y) (at level 40). +Notation "x ++++ y" := (plus x y) : A_scope. +Open Scope A_scope. +Notation "'FOO' x" := (S x) (at level 40). +Goal (2 ++++ 3) = 5. +reflexivity. +Abort. + +(* Check correct failure handling when a non-constructor notation is + used in cases pattern (bug #2724 in 8.3 and 8.4beta) *) + +Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Fail Check fun x => match x with S (FORALL x, _) => 0 end. + +(* Bug #2708: don't check for scope of variables used as binder *) + +Parameter traverse : (nat -> unit) -> (nat -> unit). +Notation traverse_var f l := (traverse (fun l => f l) l). |