feat: ForIn instance for NameMap and PersistentHashMap

src/Init/Core.lean

@@ -83,6 +83,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
 inductive ForInStep (α : Type u) where
   | done  : α → ForInStep α
   | yield : α → ForInStep α
+  deriving Inhabited
 
 class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) where
   forIn {β} [Monad m] (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

src/Lean/Data/Name.lean

@@ -154,6 +154,9 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
 
 @[inline] def find? (m : NameMap α) (n : Name) : Option α := Std.RBMap.find? m n
 
+instance : ForIn m (NameMap α) (Name × α) :=
+  inferInstanceAs (ForIn _ (Std.RBMap ..) ..)
+
 end NameMap
 
 def NameSet := RBTree Name Name.quickCmp

src/Std/Data/PersistentHashMap.lean

@@ -279,6 +279,20 @@ variable {σ : Type w}
 
 @[specialize] def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
   Id.run $ map.foldlM f init
+
+@[specialize] protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
+    (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
+  let intoError : ForInStep σ → Except σ σ
+  | .done s => .error s
+  | .yield s => .ok s
+  let result ← foldlM (m := ExceptT σ m) map (init := init) fun s a b =>
+    (intoError <$> f (a, b) s : m _)
+  match result with
+  | .ok s | .error s => pure s
+
+instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashMap α β) (α × β) where
+  forIn := PersistentHashMap.forIn
+
 end
 
 def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=