def LeanRedis.Client.ping {τ : Type} [Transport.Transport τ] (client : Client τ) (message? : Option String := none) : Std.Internal.IO.Async.Async (Option String)

Send PING and decode the optional message payload returned by Redis.

Example:

let pong ← client.ping
let echoed ← client.ping (some "hello")

Equations

• client.ping message? = do let reply ← client.execute (LeanRedis.Command.ping message?).request liftM ((LeanRedis.Command.ping message?).decode reply)

def LeanRedis.Client.auth {τ : Type} [Transport.Transport τ] (client : Client τ) (auth : AuthConfig) : Std.Internal.IO.Async.Async Unit

Send AUTH using the provided credentials.

Example:

let _ ← client.auth { password := "secret" }

Equations

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

def LeanRedis.Client.select {τ : Type} [Transport.Transport τ] (client : Client τ) (database : UInt32) : Std.Internal.IO.Async.Async Unit

Send SELECT and update the tracked selected database on success.

Example:

let _ ← client.select 2

Equations

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