structure LeanRedis.Client.EventMetadata : Type

• timestamp : Std.Time.PlainDateTime
• error? : Option Error
• attempt? : Option Nat

@[implicit_reducible]

instance LeanRedis.Client.instReprEventMetadata : Repr EventMetadata

Equations

• LeanRedis.Client.instReprEventMetadata = { reprPrec := LeanRedis.Client.instReprEventMetadata.repr }

def LeanRedis.Client.instReprEventMetadata.repr : EventMetadata → Nat → Std.Format

Equations

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

inductive LeanRedis.Client.Event : Type

• initialConnectFailed (metadata : EventMetadata) : Event
• remoteDisconnected (reason : Transport.DisconnectReason) (metadata : EventMetadata) : Event
• reconnectAttemptStarted (metadata : EventMetadata) : Event
• reconnectAttemptFailed (metadata : EventMetadata) : Event
• reconnectScheduled (delayMs : UInt32) (metadata : EventMetadata) : Event
• reconnected (metadata : EventMetadata) : Event
• reconnectStopped (metadata : EventMetadata) : Event
• explicitlyDisconnected (metadata : EventMetadata) : Event

@[implicit_reducible]

instance LeanRedis.Client.instReprEvent : Repr Event

Equations

• LeanRedis.Client.instReprEvent = { reprPrec := LeanRedis.Client.instReprEvent.repr }

def LeanRedis.Client.instReprEvent.repr : Event → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev LeanRedis.Client.EventHandler : Type

Equations

• LeanRedis.Client.EventHandler = (LeanRedis.Client.Event → Std.Internal.IO.Async.Async Unit)