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]
[EqOfCmpWrt κ β cmp]
:
MonadDStore κ β (StateT (DRBMap κ β cmp) m)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadDStoreStateRefT'DRBMapOfMonadLiftTSTOfMonadOfEqOfCmpWrt
{ω : Type}
{m : Type → Type}
{κ : Type}
{β : κ → Type}
{cmp : κ → κ → Ordering}
[MonadLiftT (ST ω) m]
[Monad m]
[EqOfCmpWrt κ β cmp]
:
MonadDStore κ β (StateRefT' ω (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]
:
MonadStore κ α (StateT (Lean.RBMap κ α cmp) m)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreStateRefT'RBMapOfMonadLiftTSTOfMonad
{ω : Type}
{m : Type → Type}
{κ α : Type}
{cmp : κ → κ → Ordering}
[MonadLiftT (ST ω) m]
[Monad m]
:
MonadStore κ α (StateRefT' ω (Lean.RBMap κ α cmp) m)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreStateRefT'RBArrayOfMonadLiftTSTOfMonad
{ω : Type}
{m : Type → Type}
{κ α : Type}
{cmp : κ → κ → Ordering}
[MonadLiftT (ST ω) m]
[Monad m]
:
MonadStore κ α (StateRefT' ω (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]
:
MonadStore Lean.Name α (StateT (Lean.NameMap α) m)
Equations
- One or more equations did not get rendered due to their size.
instance
Lake.instMonadStoreNameStateRefT'NameMapOfMonadLiftTSTOfMonad
{ω : Type}
{m : Type → Type}
{α : Type}
[MonadLiftT (ST ω) m]
[Monad m]
:
MonadStore Lean.Name α (StateRefT' ω (Lean.NameMap α) m)
Equations
- One or more equations did not get rendered due to their size.
@[inline]
instance
Lake.instMonadStore1OfOfMonadDStoreOfFamilyOut
{κ : Type u_1}
{β : κ → Type u_2}
{m : Type u_2 → Type u_3}
{k : κ}
{α : Type u_2}
[MonadDStore κ β m]
[t : FamilyOut β k α]
:
MonadStore1Of k α m
Equations
- Lake.instMonadStore1OfOfMonadDStoreOfFamilyOut = { fetch? := cast ⋯ (Lake.fetch? k), store := fun (a : α) => Lake.store k (cast ⋯ a) }