diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index bb429e1259..7c02ef0061 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -87,6 +87,11 @@ def switch (m : SMap α β) : SMap α β :=
 @[inline] def foldStage2 {σ : Type w} (f : σ → α → β → σ) (s : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f s
 
+/-- Monadic fold over a staged map. -/
+def foldM {m : Type w → Type w} [Monad m]
+    (f : σ → α → β → m σ) (init : σ) (map : SMap α β) : m σ := do
+  map.map₂.foldlM f (← map.map₁.foldM f init)
+
 def fold {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f $ m.map₁.fold f init