From 8c1cea17e3685633a44421b5039ef4f513747023 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 1 May 2025 13:34:27 -0400
Subject: [PATCH] fix(goal): Over-eager deduplication of goals

---
 Pantograph/Goal.lean | 3 +--
 Test/Metavar.lean    | 8 ++++----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 38057be..c1935cb 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -140,8 +140,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
   -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
   let unassigned := goals.filter λ goal =>
     let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
-    let isDuplicate := state.goals.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
+    ¬ isSolved
   return {
     state with
     savedState := {
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 8322abf..8659fdf 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -238,21 +238,21 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
   --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
-  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
+  let coupled_goals := coupled_goals.map (·.name.toString)
+  let coupled_goals := coupled_goals.map ({ name := ·.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar