From da06bb660569f6d6c443fc737794ddecd7fee13b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Jan 2022 08:47:05 -0800
Subject: [PATCH] fix: matching inside new `termination_by`

---
 src/Lean/Elab/PreDefinition/WF/Rel.lean |  2 +-
 tests/lean/run/955.lean                 | 26 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/955.lean

diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 8d9cf66bd3..488cec2f4a 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -57,7 +57,7 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (wf?
       let pendingMVarIds ← getMVars wfRel
       discard <| logUnassignedUsingErrorInfos pendingMVarIds
       return wfRel
-  | some (TerminationWF.ext elements) => withRef (getRefFromElems elements) do
+  | some (TerminationWF.ext elements) => withDeclName unaryPreDef.declName <| withRef (getRefFromElems elements) do
     let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
     let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
     let (d, fMVarId) ← intro1 fMVarId
diff --git a/tests/lean/run/955.lean b/tests/lean/run/955.lean
new file mode 100644
index 0000000000..befc5ed3e3
--- /dev/null
+++ b/tests/lean/run/955.lean
@@ -0,0 +1,26 @@
+namespace Ex2
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by _ n =>
+  match n with
+  | _ => n
+end Ex2
+
+
+namespace Ex3
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by' measure (fun n => match n with | Sum.inl n => n | Sum.inr n => n)
+end Ex3