Documentation

Lake.Util.Store

class Lake.MonadStore1 {κ : Type u} (k : κ) (α : outParam (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
    class Lake.MonadDStore (κ : Type u) (β : outParam (κType v)) (m : Type v → Type w) :
    Type (max (max u v) w)

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

    • fetch? : (key : κ) → m (Option (β key))
    • store : (key : κ) → β keym PUnit
    Instances
      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
      @[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
      Instances For
        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] :
        Equations
        @[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
        • One or more equations did not get rendered due to their size.
        Instances For