Util.UnorderedArraySet: remove quadratic BEq instance (#162)

leanprover-community · Sep 29, 2024 · 50aaaf7 · 50aaaf7
1 parent a895713
commit 50aaaf7
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Util.Basic
+import Batteries.Data.Array.Basic
 import Lean.Elab.Term
 import Lean.Meta.Tactic.Simp
 

diff --git a/Aesop/Util/UnorderedArraySet.lean b/Aesop/Util/UnorderedArraySet.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-import Batteries.Data.Array.Basic
 import Batteries.Data.Array.Merge
 import Lean.Message
 
@@ -131,9 +130,6 @@ def all (p : α → Bool) (s : UnorderedArraySet α) (start := 0) (stop := s.siz
     Bool :=
   s.rep.all p start stop
 
-instance : BEq (UnorderedArraySet α) where
-  beq s t := s.rep.equalSet t.rep
-
 instance [ToString α] : ToString (UnorderedArraySet α) where
   toString s := toString s.rep