diff options
Diffstat (limited to 'test-suite/success/Notations.v')
| -rw-r--r-- | test-suite/success/Notations.v | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 4bdd579a..661a8757 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -14,7 +14,7 @@ Parameter P : Type -> Type -> Type -> Type. Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). Check (nat |= nat --> nat). -(* Check that first non empty definition at an empty level can be of any +(* Check that first non empty definition at an empty level can be of any associativity *) Definition marker := O. @@ -30,4 +30,32 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2). (* Check import of notations from within a section *) Notation "+1 x" := (S x) (at level 25, x at level 9). -Section A. Global Notation "'Z'" := O (at level 9). End A. +Section A. Require Import make_notation. End A. + +(* Check use of "$" (see bug #1961) *) + +Notation "$ x" := (id x) (at level 30). +Check ($ 5). + +(* Check regression of bug #2087 *) + +Notation "'exists' x , P" := (x, P) + (at level 200, x ident, right associativity, only parsing). + +Definition foo P := let '(exists x, Q) := P in x = Q :> nat. + +(* Check empty levels when extending binder_constr *) + +Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat + (at level 200, x ident, right associativity, y at level 69). + +(* This used to loop at some time before r12491 *) + +Notation R x := (@pair _ _ x). +Check (fun x:nat*nat => match x with R x y => (x,y) end). + +(* Check multi-tokens recursive notations *) + +Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). +Check [ 0 ]. +Check [ 0 # ; 1 ]. |