From fb30932ca7a88cb713e15e4557205dfff8a1a9da Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 21 Nov 2023 19:26:52 +0100
Subject: [PATCH] refactor: WF.Fix: Pass all remaining goals to
 `Term.reportUnsolvedGoals` (#2922)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This only really shows up when the `decreasing_tactic` fails with
multiple goals, as in
```
macro_rules
  | `(tactic|decreasing_tactic) => `(tactic| by_cases (2 > 1))
def foo (n : Nat) : Nat := foo (n - 1)
termination_by foo n => n
```
where we now get
```
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n


case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
rather than
```
LeanProject.lean:3:27

unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n

LeanProject.lean:3:27

unsolved goals
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```

The effect is neglectible, but the code is a bit nicer, so why not,
before someone looks at it again and wonders whether the goals are
reported separately for a reason.
---
 src/Lean/Elab/PreDefinition/WF/Fix.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index eed16d3e65..e553ba3987 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -20,7 +20,8 @@ open Meta
 private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
   let remainingGoals ← Tactic.run mvarId do
     Tactic.evalTactic (← `(tactic| decreasing_tactic))
-  remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId]
+  unless remainingGoals.isEmpty do
+    Term.reportUnsolvedGoals remainingGoals
 
 private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
   let mvar ← mkFreshExprSyntheticOpaqueMVar decreasingProp