From 7809fe0b0143ae0f93bf0262dbc20038ff861bd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Sep 2020 11:34:53 -0700
Subject: [PATCH] fix: `def`+`match` macro

---
 src/Lean/Elab/MutualDef.lean | 2 +-
 tests/lean/run/match1.lean   | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index c20c9f0565..1a513a422f 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -126,7 +126,7 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax :=
 if declVal.isOfKind `Lean.Parser.Command.declValSimple then
   pure $ declVal.getArg 1
 else if declVal.isOfKind `Lean.Parser.Command.declValEqns then
-  expandMatchAltsIntoMatch declVal (declVal.getArg 1)
+  expandMatchAltsIntoMatch declVal (declVal.getArg 0)
 else
   Macro.throwError declVal "unexpected definition value"
 
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index cf4a25b428..aae7cb8cd6 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -26,3 +26,11 @@ theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
 by intro
  | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
  | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
+
+inductive C
+| mk₁ : Nat → C
+| mk₂ : Nat → Nat → C
+
+def C.x : C → Nat
+| C.mk₁ x   => x
+| C.mk₂ x _ => x