From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- test-suite/output/Notations3.out | 2 ++ test-suite/output/Notations3.v | 7 +++++++ 2 files changed, 9 insertions(+) (limited to 'test-suite/output') diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 5bb77b8fd..fb2d375c2 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -195,3 +195,5 @@ fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat {{{x, y}} : nat * nat | x + y = 0} : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 201198b3e..46e0c1b1b 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -337,3 +337,10 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) Check {(x,y)|x+y=0}. + +Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x pattern, p at level 200, right associativity, + format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + +Check exists2' (x,y), x=0 & y=0. -- cgit v1.2.3