def LeanRedis.Client.execute {τ : Type} [Transport.Transport τ] (client : Client τ) (request : CommandRequest) : Std.Internal.IO.Async.Async Protocol.Resp.Value

Execute a single command and return its Redis response value.

Example:

let reply ← client.execute (Command.ping ()).request

Equations

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

def LeanRedis.Client.runPipeline {τ : Type} {α : List Type} [Transport.Transport τ] (client : Client τ) (pipeline : Pipeline α) : Std.Internal.IO.Async.Async (HList α)

Execute a pipeline.

Example:

 (a,b,_) ← client.runPipeline <| Pipeline.empty |>.get "hello" |>.set "bar" "baz" |>.get "bar"

Equations

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

def LeanRedis.Client.new {τ : Type} [Transport.Transport τ] (config : Config) : IO (Client τ)

Create a new client value for the given transport type without opening a connection.

Example:

let client : LeanRedis.Client MyTransport ← LeanRedis.Client.new cfg

Equations

• LeanRedis.Client.new config = do let state ← liftM (Std.Mutex.new { config := config }) let subscribers ← liftM (Std.Mutex.new { }) pure { state := state, subscribers := subscribers }

def LeanRedis.Client.newDefault (config : Config) : IO (Client Transport.TCP)

Create a new client using the default TCP transport without opening a connection.

Example:

let client ← LeanRedis.Client.newDefault {
  endpoint := { host := "127.0.0.1", port := 6379 }
}

Equations

• LeanRedis.Client.newDefault config = LeanRedis.Client.new config

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

Open the transport and run Redis bootstrap for an existing client.

If a reconnect wait is in progress, this cancels it logically and tries immediately.

Example:

let _ ← client.connect

Equations

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

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

Close the current connection and stop background reconnects until a later explicit connect.

Example:

let _ ← client.disconnect

Equations

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

def LeanRedis.Client.isConnected {τ : Type} (client : Client τ) : Std.Internal.IO.Async.Async Bool

Return true when the client currently has a ready runtime.

Example:

let connected ← client.isConnected

Equations

• client.isConnected = do let state ← LeanRedis.Client.getState✝ client pure state.session.isReady

def LeanRedis.Client.connectionStatus {τ : Type} (client : Client τ) : Std.Internal.IO.Async.Async Protocol.Phase

Return the current lifecycle status of the client.

Example:

let status ← client.connectionStatus

Equations

• client.connectionStatus = do let state ← LeanRedis.Client.getState✝ client pure state.session.phase

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

Fail with an unavailable error unless the client is connected.

Example:

let _ ← client.requireConnected

Equations

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

def LeanRedis.Client.currentState {τ : Type} (client : Client τ) : Std.Internal.IO.Async.Async Protocol.Session

Read the current internal connection state tracked by the client.

Example:

let state ← client.currentState

Equations

• client.currentState = do let state ← LeanRedis.Client.getState✝ client pure state.session

def LeanRedis.Client.onEvent {τ : Type} (client : Client τ) (handler : EventHandler) : IO ClientEventSubscriptionId

Subscribe an async handler to client connection lifecycle events.

Returns a subscription id that can later be passed to offEvent.

Example:

let sub ← client.onEvent fun event => do
  IO.println s!"{repr event}"

Equations

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

def LeanRedis.Client.offEvent {τ : Type} (client : Client τ) (subscriptionId : ClientEventSubscriptionId) : IO Unit

Remove a previously registered event handler.

Example:

let sub ← client.onEvent fun _ => pure ()
client.offEvent sub

Equations

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