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