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)
Equations
- One or more equations did not get rendered due to their size.
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)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreStateTRBArray
{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.instMonadStoreNameStateTNameMap
{m : Type → Type u_1}
{α : Type}
[Monad m]
:
Lake.MonadStore Lake.Name α (StateT (Lake.NameMap α) m)
Equations
- Lake.instMonadStoreNameStateTNameMap = inferInstanceAs (Lake.MonadStore Lake.Name α (StateT (Lean.RBMap Lake.Name α Lean.Name.quickCmp) 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
Equations
- Lake.instMonadStore1_1 = { fetch? := cast (_ : m (Option (β k)) = m (Option α)) (Lake.fetch? k), store := fun a => Lake.store k (cast (_ : α = β k) a) }