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.
class
Lake.MonadStore1
{κ : Type u}
(k : κ)
(α : outParam (Type v))
(m : Type v → Type w)
:
Type (max v w)
Similar to MonadStore1Of, but α is an outParam for convenience.
Instances
instance
Lake.instMonadStore1OfMonadStore1Of :
{κ : Type u_1} →
{k : κ} → {α : Type u_2} → {m : Type u_2 → Type u_3} → [inst : Lake.MonadStore1Of k α m] → Lake.MonadStore1 k α m
Equations
- Lake.instMonadStore1OfMonadStore1Of = { fetch? := Lake.MonadStore1Of.fetch? k, store := Lake.store k }
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.
instance
Lake.instMonadStore1OfOfMonadDStore
{κ : Type u_1}
{β : κ → Type u_2}
{m : Type u_2 → Type u_3}
{k : κ}
[Lake.MonadDStore κ β m]
:
Lake.MonadStore1Of k (β k) m
Equations
- Lake.instMonadStore1OfOfMonadDStore = { fetch? := Lake.MonadDStore.fetch? k, store := fun (o : β k) => Lake.MonadDStore.store k o }
@[reducible, inline]
abbrev
Lake.MonadStore
(κ : Type u_1)
(α : Type u_2)
(m : Type u_2 → Type u_3)
:
Type (max (max u_1 u_2) u_3)
A monad equipped with a key-object store.
Equations
- Lake.MonadStore κ α m = Lake.MonadDStore κ (fun (x : κ) => α) m
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]
[Lake.MonadDStore κ β m]
:
Lake.MonadDStore κ β n
Equations
- Lake.instMonadDStoreOfMonadLift = { fetch? := fun (k : κ) => liftM (Lake.fetch? k), store := fun (k : κ) (a : β k) => liftM (Lake.store k a) }
@[inline]
def
Lake.fetchOrCreate
{m : Type u_1 → Type u_2}
{κ : Type u_3}
{α : Type u_1}
[Monad m]
(key : κ)
[Lake.MonadStore1Of key α m]
(create : m α)
:
m α
Equations
- Lake.fetchOrCreate key create = do let __do_lift ← Lake.fetch? key match __do_lift with | some val => pure val | x => do let val ← create Lake.store key val pure val