From 96b2ad46828380c8558440f8adf9eb996e440535 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 13 Nov 2024 16:35:29 +1100
Subject: [PATCH] chore: remove duplicate NameMap forIn instance

---
 Batteries/Lean/NameMap.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Batteries/Lean/NameMap.lean b/Batteries/Lean/NameMap.lean
index 7ca7e7acea..0c6d341925 100644
--- 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`.