From d3de12fa092afc1f2f7d658975e783f8cd490274 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Sep 2020 16:51:46 -0700
Subject: [PATCH] test: another dependent pattern matching test

---
 tests/lean/run/match1.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index 65a8a838ad..8aeb5e635a 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -96,3 +96,12 @@ def Foo.addY? : Foo × Foo → Option Nat
 
 theorem ex8 : Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) = some 22 :=
 rfl
+
+instance {α} : Inhabited (Sigma fun m => Vec α m) :=
+⟨⟨0, Vec.nil⟩⟩
+
+partial def filter {α} (p : α → Bool) : {n : Nat} → Vec α n → Sigma fun m => Vec α m
+| _, Vec.nil        => ⟨0, Vec.nil⟩
+| _, Vec.cons x xs  => match p x, filter p xs with
+  | true,  ⟨_, ys⟩ => ⟨_, Vec.cons x ys⟩
+  | false, ys      => ys