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

Equations

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

def LeanRedis.CacheSWR.newDefault (config : Config) : Std.Async.Async (CacheSWR Transport.TCP)

Equations

• LeanRedis.CacheSWR.newDefault config = LeanRedis.CacheSWR.new config

@[inline, specialize #[]]

def LeanRedis.CacheSWR.get {τ : Type} [Transport.Transport τ] (cache : CacheSWR τ) (key : String) (cb : Unit → Std.Async.Async String) (opts : CacheSWROptions) : Std.Async.Async String

Gets a value from the cache by key.

• If a fresh value is found, it is returned immediately.
• If a stale value is found, it is returned immediately and a background refresh is triggered to update the cache.
• 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 requests request the same key concurrently.
• Cache stampedes are prevented.

Equations

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