chore: cleanup

leanprover-community · May 27, 2024 · a59a726 · a59a726
1 parent 2e64898
commit a59a726
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 32 deletions.
diff --git a/Batteries.lean b/Batteries.lean
@@ -34,7 +34,6 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
-import Batteries.Data.Sigma
 import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt

diff --git a/Batteries/Data/DArray.lean b/Batteries/Data/DArray.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
 
-import Batteries.Data.Sigma
-
 namespace Batteries
 
 /-- `DArray` is a heterogenous array with element types given by `type`. -/

diff --git a/Batteries/Data/Sigma.lean b/Batteries/Data/Sigma.lean