class
Lake.MonadStore1Of
{κ : Type u}
(k : κ)
(α : semiOutParam (Type v))
(m : Type v → Type w)
:
Type (max v w)
A monad equipped with a dependently typed key-value store for a particular key.
Instances
instance
Lake.instMonadStore1OfMonadStore1Of
{κ✝ : Type u_1}
{k : κ✝}
{α : Type u_2}
{m : Type u_2 → Type u_3}
[MonadStore1Of k α m]
:
MonadStore1 k α m
Equations
class
Lake.MonadDStore
(κ : Type u)
(β : semiOutParam (κ → Type v))
(m : Type v → Type w)
:
Type (max (max u v) w)
A monad equipped with a dependently typed key-object store.
Instances
instance
Lake.instMonadStore1OfOfMonadDStore
{κ : Type u_1}
{β : κ → Type u_2}
{m : Type u_2 → Type u_3}
{k : κ}
[MonadDStore κ β m]
:
MonadStore1Of k (β k) m
Equations
instance
Lake.instMonadDStoreOfMonadLift
{m : Type u_1 → Type u_2}
{n : Type u_1 → Type u_3}
{κ : Type u_4}
{β : κ → Type u_1}
[MonadLift m n]
[MonadDStore κ β m]
:
MonadDStore κ β n
Equations
@[inline]
def
Lake.fetchOrCreate
{m : Type u_1 → Type u_2}
{κ : Type u_3}
{α : Type u_1}
[Monad m]
(key : κ)
[MonadStore1Of key α m]
(create : m α)
:
m α