chore: remove TODO

leanprover · Jan 13, 2025 · 339d12f · 339d12f
1 parent ca1790c
commit 339d12f
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset.lean
@@ -213,8 +213,7 @@ def internalizeCnstr (e : Expr) : GoalM Unit := do
       return ()
   if let some k ← getDist? v u then
     if (← propagateFalse v u k c e) then
-      -- TODO: constraint was assigned `False`, we don't need to register it
-      pure ()
+      return ()
   trace[grind.offset.internalize] "{e} ↦ {c}"
   modify' fun s => { s with
     cnstrs   := s.cnstrs.insert { expr := e } c