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] [EqOfCmpWrt κ β cmp] :
MonadDStore κ β (StateT (DRBMap κ β cmp) m)
Equations
    instance Lake.instMonadDStoreStateRefT'DRBMapOfMonadLiftTSTOfMonadOfEqOfCmpWrt {ω : Type} {m : TypeType} {κ : Type} {β : κType} {cmp : κκOrdering} [MonadLiftT (ST ω) m] [Monad m] [EqOfCmpWrt κ β cmp] :
    MonadDStore κ β (StateRefT' ω (DRBMap κ β cmp) m)
    Equations
      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
        instance Lake.instMonadStoreStateRefT'RBMapOfMonadLiftTSTOfMonad {ω : Type} {m : TypeType} {κ α : Type} {cmp : κκOrdering} [MonadLiftT (ST ω) m] [Monad m] :
        MonadStore κ α (StateRefT' ω (Lean.RBMap κ α cmp) m)
        Equations
          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] :
          MonadStore κ α (StateT (RBArray κ α cmp) m)
          Equations
            instance Lake.instMonadStoreStateRefT'RBArrayOfMonadLiftTSTOfMonad {ω : Type} {m : TypeType} {κ α : Type} {cmp : κκOrdering} [MonadLiftT (ST ω) m] [Monad m] :
            MonadStore κ α (StateRefT' ω (RBArray κ α cmp) m)
            Equations
              @[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 α] :
              Equations