diff options
Diffstat (limited to 'test-suite/success/Notations2.v')
| -rw-r--r-- | test-suite/success/Notations2.v | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 08d904cea..7c2cf3ee5 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). (* 11. Notations with needed factorization of a recursive pattern *) (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) -Module A. +Module M11. Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). Check [:: 1 ; 2 ; 3 ]. Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) -End A. +End M11. (* 12. Preventively check that a variable which does not occur can be instantiated *) (* by any term. In particular, it should not be restricted to a binder *) @@ -111,3 +111,18 @@ Module M12. Notation "N ++ x" := (S x) (only parsing). Check 2 ++ 0. End M12. + +(* 13. Check that internal data about associativity are not used in comparing levels *) +Module M13. +Notation "x ;; z" := (x + z) + (at level 100, z at level 200, only parsing, right associativity). +Notation "x ;; z" := (x * z) + (at level 100, z at level 200, only parsing) : foo_scope. +End M13. + +(* 14. Check that a notation with a "ident" binder does not include a pattern *) +Module M14. +Notation "'myexists' x , p" := (ex (fun x => p)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. +Check myexists I, I = 0. (* Should not be seen as a constructor *) +End M14. |