Documentation

Mathlib.Lean.SMap

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
Instances For