structure LeanRedis.Connection.DriverState (τ : Type) : Type

• transport? : Option τ
• parser : Protocol.Resp.Parse.ParserState
• session : Protocol.Session
• config : Config

@[implicit_reducible]

instance LeanRedis.Connection.instInhabitedDriverState {a✝ : Type} : Inhabited (DriverState a✝)

Equations

• LeanRedis.Connection.instInhabitedDriverState = { default := LeanRedis.Connection.instInhabitedDriverState.default }

def LeanRedis.Connection.instInhabitedDriverState.default {a✝ : Type} : DriverState a✝

Equations

• LeanRedis.Connection.instInhabitedDriverState.default = { transport? := default, parser := default, session := default }

def LeanRedis.Connection.readSize : UInt64

Equations

• LeanRedis.Connection.readSize = 4096

def LeanRedis.Connection.onRemoteDisconnect {τ : Type} (state : DriverState τ) : DriverState τ × Array Protocol.Effect

Equations

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

def LeanRedis.Connection.onReconnectExhausted {τ : Type} (state : DriverState τ) : DriverState τ × Array Protocol.Effect

Equations

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

def LeanRedis.Connection.onTransportFailed {τ : Type} (state : DriverState τ) (error : String) : DriverState τ × Array Protocol.Effect

Equations

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

def LeanRedis.Connection.onConnectRequest {τ : Type} (state : DriverState τ) : DriverState τ × Array Protocol.Effect

Equations

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

def LeanRedis.Connection.executeCommand {τ : Type} [Transport.Transport τ] (request : CommandRequest) (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Protocol.Resp.Value)

Equations

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

def LeanRedis.Connection.executeBatch {τ : Type} [Transport.Transport τ] (requests : Array CommandRequest) (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Array Protocol.Resp.Value)

Equations

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

def LeanRedis.Connection.connectBootstrap {τ : Type} [Transport.Transport τ] (transport : τ) (config : Config) (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Array Protocol.Effect)

Equations

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

def LeanRedis.Connection.connectTransport {τ : Type} [Transport.Transport τ] (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Array Protocol.Effect)

Equations

• LeanRedis.Connection.connectTransport state = do let transport ← LeanRedis.Transport.Transport.connect state.config.endpoint LeanRedis.Connection.connectBootstrap transport state.config state

def LeanRedis.Connection.tryReconnect {τ : Type} [Transport.Transport τ] (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Array Protocol.Effect)

Equations

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

def LeanRedis.Connection.disconnect {τ : Type} [Transport.Transport τ] (state : DriverState τ) : Std.Internal.IO.Async.Async (DriverState τ × Array Protocol.Effect)

Equations

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