Documentation

Lake.Util.StoreInsts

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.
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} [Lake.MonadDStore κ β m] [t : Lake.FamilyOut β k α] :
Equations