More import pruning

leanprover · Feb 22, 2024 · cfc4fdd · cfc4fdd
1 parent e83285b
commit cfc4fdd
Showing 1 changed file with 0 additions and 4 deletions.
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