Documentation

Lake.Util.Store

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
    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} [MonadStore1Of 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.

        • fetch? (key : κ) : m (Option (β key))
        • store (key : κ) : β keym PUnit
        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
            @[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
              Instances For
                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 α
                  Equations
                    Instances For