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} → [inst : Lake.MonadStore1Of k α m] → Lake.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.

      • 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 : κ} [Lake.MonadDStore κ β 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] [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.MonadStore1Of key α m] (create : m α) :
          m α
          Equations
          Instances For