diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 20:50:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
| tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /test-suite/success | |
| parent | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (diff) | |
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
Diffstat (limited to 'test-suite/success')
| -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. |