aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-15 18:32:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:05 +0100
commit398358618bb3eabfe822b79c669703c1c33b67e6 (patch)
tree967c18294374fe73a51d582cd120ab70eb856936 /test-suite
parente21f70cc2b284a3cf489b16e0251492fb864cf1e (diff)
Adding patterns in the category of binders for notations.
For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"...
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Notations3.out2
-rw-r--r--test-suite/output/Notations3.v4
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 9c711ff26..5bb77b8fd 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -193,3 +193,5 @@ 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
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d81cc702a..201198b3e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -333,3 +333,7 @@ Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
(match t with S n => p | 0 => q end)
(at level 200).
Check fun x => if x is n.+1 then n else 1.
+
+(* Examples with binding patterns *)
+
+Check {(x,y)|x+y=0}.