chore: cleanup

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

Hide file tree

Showing 4 changed files with 2 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
diff --git a/test/darray.lean b/test/darray.lean
@@ -2,6 +2,8 @@ import Batteries.Data.DArray
 
 open Batteries
 
+set_option trace.compiler.ir.result true
+
 def foo : DArray 3 fun | 0 => String | 1 => Nat | 2 => Array Nat :=
   .mk fun | 0 => "foo" | 1 => 42 | 2 => #[4, 2]