instance
Lake.instMonadDStoreStateTDRBMapOfMonadOfEqOfCmpWrt
{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)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreStateTRBMapOfMonad
{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)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreStateTRBArrayOfMonad
{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 (Lake.RBArray κ α cmp) m)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreNameStateTNameMapOfMonad
{m : Type → Type u_1}
{α : Type}
[Monad m]
:
Lake.MonadStore Lake.Name α (StateT (Lake.NameMap α) m)
Equations
- Lake.instMonadStoreNameStateTNameMapOfMonad = inferInstanceAs (Lake.MonadStore Lake.Name α (StateT (Lean.RBMap Lake.Name α Lean.Name.quickCmp) m))
@[inline]
instance
Lake.instMonadStore1OfMonadDStoreOfFamilyOut
{κ : 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
Equations
- Lake.instMonadStore1OfMonadDStoreOfFamilyOut = { fetch? := cast ⋯ (Lake.fetch? k), store := fun (a : α) => Lake.store k (cast ⋯ a) }