aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-29 18:30:50 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-29 18:45:46 +0200
commit8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (patch)
tree0875a95610c22592eaf52a15bb0d9dd502aad914 /test-suite
parente128900aee63c972d7977fd47e3fd21649b63409 (diff)
Fixes #7110 ("as" untested while looking for notation for nested patterns).
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Notations3.out8
-rw-r--r--test-suite/output/Notations3.v16
2 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 1987b6a6e..304353f55 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,3 +223,11 @@ fun S : nat => [[S | S.S]]
: Set
exists2 '{{y, z}} : nat * nat, y > z & z > y
: Prop
+foo =
+fun l : list nat => match l with
+ | _ :: (_ :: _) as l1 => l1
+ | _ => l
+ end
+ : list nat -> list nat
+
+Argument scope is [list_scope]
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c165f9553..d2d136946 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,10 +278,12 @@ Set Printing Notations.
(* Check insensitivity of "match" clauses to order *)
+Module IfPat.
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.
+End IfPat.
(* Examples with binding patterns *)
@@ -338,11 +340,13 @@ Check ∀ '(((x,y),true)|((x,y),false)), x>y.
(* Check Georges' printability of a "if is then else" notation *)
+Module IfPat2.
Notation "'if' c 'is' p 'then' u 'else' v" :=
(match c with p => u | _ => v end)
(at level 200, p pattern at level 100).
Check fun p => if p is S n then n else 0.
Check fun p => if p is Lt then 1 else 0.
+End IfPat2.
(* Check that mixed binders and terms defaults to ident and not pattern *)
Module F.
@@ -364,3 +368,15 @@ Check {'(x,y)|x+y=0}.
(* Check exists2 with a pattern *)
Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+
+Module Issue7110.
+Open Scope list_scope.
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+ (at level 0).
+Definition foo (l : list nat) :=
+ match l with
+ | a :: (b :: l) as l1 => l1
+ | _ => l
+end.
+Print foo.
+End Issue7110.