remove unused includes to fix build

leanprover-community · Nov 4, 2024 · b28f0d7 · b28f0d7
1 parent 4d927e0
commit b28f0d7
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/Mathlib/Data/Fin/Tuple/Take.lean b/Mathlib/Data/Fin/Tuple/Take.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Quang Dao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Quang Dao
 -/
-import Batteries.Data.List.OfFn
 import Mathlib.Data.Fin.Tuple.Basic
 
 /-!

diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Batteries.Data.List.OfFn
 import Mathlib.Data.Fin.Tuple.Basic
 
 /-!