removed default_instance from ArrayN GetElem instance

lecopivo · Aug 20, 2024 · fbff9a6 · fbff9a6
1 parent 7343de5
commit fbff9a6
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/SciLean/Data/ArrayN.lean b/SciLean/Data/ArrayN.lean
@@ -4,7 +4,6 @@ structure ArrayN (α : Type) (n : Nat) where
   data : Array α
   h_size : n = data.size
 
-@[default_instance]
 instance : GetElem (ArrayN α n) (Fin n) α (λ _ _ => True) where
   getElem arr i _ := arr.data.get (arr.h_size ▸ i)