diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index d513fe0ae0..7c6a12393b 100644
--- a/src/Init/Core.lean
+++ b/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 β
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index a60c037cce..5c6c092db9 100644
--- a/src/Lean/Data/Name.lean
+++ b/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
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index 2c181174c0..6e5b736fcc 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/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 (α × β) :=