Extra functions on Lean.SMap #
def
Lean.SMap.foldM
{α : Type u_1}
{σ : Type w}
{β : Type u_2}
{m : Type w → Type w}
[Monad m]
[BEq α]
[Hashable α]
(f : σ → α → β → m σ)
(init : σ)
(map : Lean.SMap α β)
:
m σ
Monadic fold over a staged map.
Equations
- Lean.SMap.foldM f init map = do let __do_lift ← Lean.HashMap.foldM f init map.map₁ Lean.PersistentHashMap.foldlM map.map₂ f __do_lift