From aecebaab74e2d24500874b89b1135a366c80221d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jul 2024 03:11:58 +1000 Subject: [PATCH] chore: upstream SMap.foldM (#4690) --- src/Lean/Data/SMap.lean | 5 +++++ 1 file changed, 5 insertions(+) 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