chore: remove duplicate NameMap forIn instance (#1043)

leanprover-community · Nov 13, 2024 · 44484f9 · 44484f9
1 parent eeb25d3
commit 44484f9
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Batteries/Lean/NameMap.lean b/Batteries/Lean/NameMap.lean
@@ -13,9 +13,6 @@ We provide `NameMap.filter` and `NameMap.filterMap`.
 
 namespace Lean.NameMap
 
-instance : ForIn m (NameMap β) (Name × β) :=
-  inferInstanceAs <| ForIn m (RBMap Name β _) _
-
 /--
 `filter f m` returns the `NameMap` consisting of all
 "`key`/`val`"-pairs in `m` where `f key val` returns `true`.