instance
Lake.instMonadDStoreStateTDRBMap
{m : Type (max u_1 u_2) → Type u_3}
{κ : Type u_1}
{β : κ → Type (max u_2 u_1)}
{cmp : κ → κ → Ordering}
[Monad m]
[Lake.EqOfCmpWrt κ β cmp]
:
Lake.MonadDStore κ β (StateT (Lake.DRBMap κ β cmp) m)
instance
Lake.instMonadStoreStateTRBMap
{m : Type (max u_1 u_2) → Type u_3}
{κ : Type u_1}
{α : Type (max u_2 u_1)}
{cmp : κ → κ → Ordering}
[Monad m]
:
Lake.MonadStore κ α (StateT (Lean.RBMap κ α cmp) m)
instance
Lake.instMonadStoreNameStateTNameMap
{m : Type → Type u_1}
{α : Type}
[Monad m]
:
Lake.MonadStore Lake.Name α (StateT (Lake.NameMap α) m)
@[inline]
instance
Lake.instMonadStore1_1
{κ : Type u_1}
{β : κ → Type u_2}
{m : Type u_2 → Type u_3}
{k : κ}
{α : Type u_2}
[Lake.MonadDStore κ β m]
[t : Lake.FamilyOut β k α]
:
Lake.MonadStore1 k α m