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"