From 79adb025f16379ca08623849343c3daa12e28241 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 1 Aug 2024 16:29:02 -0400 Subject: [PATCH] Update find_TODOs.lean --- scripts/find_TODOs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean index 3b73281..1165c6b 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.Notation +import Mathlib.Init.Data.Nat.Lemmas /-! # TODO finder