refactor: reduced unsed imports (#3464)

leanprover · Feb 22, 2024 · 23d3ac4 · 23d3ac4
1 parent 5bbc544
commit 23d3ac4
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 5 deletions.
diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.NotationExtra
+import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 

diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
@@ -4,11 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Control.Except
 import Init.Data.ByteArray
-import Init.SimpLemmas
-import Init.Util
-import Init.WFTactics
 
 namespace String