Update find_TODOs.lean

This commit is contained in:
jstoobysmith 2024-08-01 16:29:02 -04:00
parent 8ed80a1367
commit 79adb025f1

View file

@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
-/ -/
import Lean import Lean
import Batteries.Data.String.Matcher import Batteries.Data.String.Matcher
import Mathlib.Init.Data.Nat.Notation import Mathlib.Init.Data.Nat.Lemmas
/-! /-!
# TODO finder # TODO finder