From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 20:50:03 +0100 Subject: 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}. --- test-suite/output/Notations3.out | 2 -- test-suite/output/Notations3.v | 2 -- 2 files changed, 4 deletions(-) (limited to 'test-suite/output') diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6d195b512..3fd4c1c31 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -194,8 +194,6 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) 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 exists2 x : nat * nat, diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b4ad4a7b3..9ea218481 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) -Check {(x,y)|x+y=0}. - Module D. Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) (at level 200, x pattern, p at level 200, right associativity, -- cgit v1.2.3