diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean index 1165c6b..6e8fbca 100644 --- a/scripts/find_TODOs.lean +++ b/scripts/find_TODOs.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import Lean import Batteries.Data.String.Matcher -import Mathlib.Init.Data.Nat.Lemmas +import Mathlib.Data.Nat.Notation /-! # TODO finder