def Inflight : Type

Equations

• Inflight = IO.Promise (Except IO.Error String)

structure Cache (τ : Type) : Type

• redis : LeanRedis.Client τ
• inflight : Std.Mutex (Std.HashMap String Inflight)

def Cache.new {τ : Type} [LeanRedis.Transport.Transport τ] (config : LeanRedis.Config) : Std.Internal.IO.Async.Async (Cache τ)

Equations

• Cache.new config = do let client ← liftM (LeanRedis.Client.new config) client.connect let inflight ← liftM (Std.Mutex.new ∅) pure { redis := client, inflight := inflight }

def Cache.newDefault (config : LeanRedis.Config) : Std.Internal.IO.Async.Async (Cache LeanRedis.Transport.TCP)

Equations

• Cache.newDefault config = Cache.new config

@[inline, specialize #[]]

def Cache.get {τ : Type} [LeanRedis.Transport.Transport τ] (cache : Cache τ) (key : String) (cb : Unit → Std.Internal.IO.Async.Async String) (options : LeanRedis.SetOptions := { }) : Std.Internal.IO.Async.Async String

Gets a value from the cache by key. If no value is found, the callback will be called to populate it. The callback is executed exactly once for each key, even if multiple threads request the same key concurrently. Cache stampedes are prevented

Equations

• One or more equations did not get rendered due to their size.