structure LeanRedis.Transport.Endpoint : Type

• host : String
• host : String
• port : UInt16
• port : UInt16

@[implicit_reducible]

instance LeanRedis.Transport.instBEqEndpoint : BEq Endpoint

Equations

• LeanRedis.Transport.instBEqEndpoint = { beq := LeanRedis.Transport.instBEqEndpoint.beq }

def LeanRedis.Transport.instBEqEndpoint.beq : Endpoint → Endpoint → Bool

Equations

• LeanRedis.Transport.instBEqEndpoint.beq { host := a, port := a_1 } { host := b, port := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.Transport.instBEqEndpoint.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Transport.instInhabitedEndpoint : Inhabited Endpoint

Equations

• LeanRedis.Transport.instInhabitedEndpoint = { default := LeanRedis.Transport.instInhabitedEndpoint.default }

def LeanRedis.Transport.instInhabitedEndpoint.default : Endpoint

Equations

• LeanRedis.Transport.instInhabitedEndpoint.default = { host := default, port := default }

def LeanRedis.Transport.instReprEndpoint.repr : Endpoint → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.Transport.instReprEndpoint : Repr Endpoint

Equations

• LeanRedis.Transport.instReprEndpoint = { reprPrec := LeanRedis.Transport.instReprEndpoint.repr }

inductive LeanRedis.Transport.DisconnectReason : Type

• closedByPeer : DisconnectReason
• closedByClient : DisconnectReason
• readFailure (message : String) : DisconnectReason
• writeFailure (message : String) : DisconnectReason

@[implicit_reducible]

instance LeanRedis.Transport.instBEqDisconnectReason : BEq DisconnectReason

Equations

• LeanRedis.Transport.instBEqDisconnectReason = { beq := LeanRedis.Transport.instBEqDisconnectReason.beq }

def LeanRedis.Transport.instBEqDisconnectReason.beq : DisconnectReason → DisconnectReason → Bool

Equations

• LeanRedis.Transport.instBEqDisconnectReason.beq LeanRedis.Transport.DisconnectReason.closedByPeer LeanRedis.Transport.DisconnectReason.closedByPeer = true
• LeanRedis.Transport.instBEqDisconnectReason.beq LeanRedis.Transport.DisconnectReason.closedByClient LeanRedis.Transport.DisconnectReason.closedByClient = true
• LeanRedis.Transport.instBEqDisconnectReason.beq (LeanRedis.Transport.DisconnectReason.readFailure a) (LeanRedis.Transport.DisconnectReason.readFailure b) = (a == b)
• LeanRedis.Transport.instBEqDisconnectReason.beq (LeanRedis.Transport.DisconnectReason.writeFailure a) (LeanRedis.Transport.DisconnectReason.writeFailure b) = (a == b)
• LeanRedis.Transport.instBEqDisconnectReason.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Transport.instInhabitedDisconnectReason : Inhabited DisconnectReason

Equations

• LeanRedis.Transport.instInhabitedDisconnectReason = { default := LeanRedis.Transport.instInhabitedDisconnectReason.default }

def LeanRedis.Transport.instInhabitedDisconnectReason.default : DisconnectReason

Equations

• LeanRedis.Transport.instInhabitedDisconnectReason.default = LeanRedis.Transport.DisconnectReason.closedByPeer

@[implicit_reducible]

instance LeanRedis.Transport.instReprDisconnectReason : Repr DisconnectReason

Equations

• LeanRedis.Transport.instReprDisconnectReason = { reprPrec := LeanRedis.Transport.instReprDisconnectReason.repr }

def LeanRedis.Transport.instReprDisconnectReason.repr : DisconnectReason → Nat → Std.Format

Equations

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

class LeanRedis.Transport.Transport (α : Type) : Type

• connect : Endpoint → Std.Internal.IO.Async.Async α
• connect : Endpoint → Std.Internal.IO.Async.Async α
• recv : α → UInt64 → Std.Internal.IO.Async.Async ByteArray
• recv : α → UInt64 → Std.Internal.IO.Async.Async ByteArray
• send : α → ByteArray → Std.Internal.IO.Async.Async Unit
• send : α → ByteArray → Std.Internal.IO.Async.Async Unit
• sendAll : α → Array ByteArray → Std.Internal.IO.Async.Async Unit
• sendAll : α → Array ByteArray → Std.Internal.IO.Async.Async Unit
• close : α → Std.Internal.IO.Async.Async Unit
• close : α → Std.Internal.IO.Async.Async Unit