class Lake.MonadStore1 {κ : Type u} (k : κ) (α : outParam (Type v)) (m : Type v → Type w) : Type (max v w)

• fetch? : m (Option α)
• store : α → m PUnit

A monad equipped with a dependently typed key-value store for a particular key.

class Lake.MonadDStore (κ : Type u) (β : outParam (κ → Type v)) (m : Type v → Type w) : Type (max (max u v) w)

• fetch? : (key : κ) → m (Option (β key))
• store : (key : κ) → β key → m PUnit

A monad equipped with a dependently typed key-object store.

instance Lake.instMonadStore1 {κ : Type u_1} {β : κ → Type u_2} {m : Type u_2 → Type u_3} {k : κ} [Lake.MonadDStore κ β m] : Lake.MonadStore1 k (β k) m

Equations

• Lake.instMonadStore1 = { fetch? := Lake.MonadDStore.fetch? k, store := fun o => Lake.MonadDStore.store k o }

@[inline, reducible]

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.instMonadDStore {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.instMonadDStore = { fetch? := fun k => liftM (Lake.fetch? k), store := fun k a => 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.MonadStore1 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