From 564d2be3b3395042167d33d14aa0e9bdcccedcb1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 3 Nov 2020 11:13:47 +0100
Subject: [PATCH] feat: KVMap.forIn

---
 src/Lean/Data/KVMap.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean
index a11bab6e60..f5ba48c691 100644
--- a/src/Lean/Data/KVMap.lean
+++ b/src/Lean/Data/KVMap.lean
@@ -130,6 +130,10 @@ def setBool (m : KVMap) (k : Name) (v : Bool) : KVMap :=
 def setName (m : KVMap) (k : Name) (v : Name) : KVMap :=
   m.insert k (DataValue.ofName v)
 
+@[inline] def forIn.{w, w'} {δ : Type w} {m : Type w → Type w'} [Monad m]
+  (kv : KVMap) (init : δ) (f : Name × DataValue → δ → m (ForInStep δ)) : m δ :=
+  kv.entries.forIn init f
+
 def subsetAux : List (Name × DataValue) → KVMap → Bool
   | [],          m₂ => true
   | (k, v₁)::m₁, m₂ =>