@[reducible, inline]

abbrev LeanRedis.ClientEventSubscriptionId : Type

Equations

• LeanRedis.ClientEventSubscriptionId = Nat

structure LeanRedis.ClientSubscribers : Type

• nextId : ClientEventSubscriptionId
• handlers : Array (ClientEventSubscriptionId × Client.EventHandler)

def LeanRedis.instInhabitedClientSubscribers.default : ClientSubscribers

Equations

• LeanRedis.instInhabitedClientSubscribers.default = { nextId := default, handlers := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedClientSubscribers : Inhabited ClientSubscribers

Equations

• LeanRedis.instInhabitedClientSubscribers = { default := LeanRedis.instInhabitedClientSubscribers.default }

structure LeanRedis.Client (τ : Type) : Type

• state : Std.Mutex (Connection.DriverState τ)
• subscribers : Std.Mutex ClientSubscribers
• subscribers : Std.Mutex ClientSubscribers