From f04f51a29534da933f5d9d96a79d576fd6365a26 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2019 13:32:57 -0800
Subject: [PATCH] test: pattern confusion example

cc @dselsam
---
 tests/elabissues/patternIssue.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/elabissues/patternIssue.lean

diff --git a/tests/elabissues/patternIssue.lean b/tests/elabissues/patternIssue.lean
new file mode 100644
index 0000000000..9ad88efeff
--- /dev/null
+++ b/tests/elabissues/patternIssue.lean
@@ -0,0 +1,13 @@
+inductive Moo : Type
+| M1 : Moo
+| M2 : Moo
+
+inductive Foo : Type
+| mk₁ : Moo → Foo
+| mk₂ : Foo
+
+def bar : Foo → String
+| Foo.mk₁ M1 => "mk₁ M1"
+| _ => "else"
+
+#eval bar (Foo.mk₁ Moo.M2) -- "mk₁ M1"