structure LeanRedis.ReconnectExponentialBackoff : Type

• baseDelayMs : UInt32
• maxDelayMs : UInt32
• jitter : Bool

def LeanRedis.instBEqReconnectExponentialBackoff.beq : ReconnectExponentialBackoff → ReconnectExponentialBackoff → Bool

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.instBEqReconnectExponentialBackoff.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqReconnectExponentialBackoff : BEq ReconnectExponentialBackoff

Equations

• LeanRedis.instBEqReconnectExponentialBackoff = { beq := LeanRedis.instBEqReconnectExponentialBackoff.beq }

def LeanRedis.instInhabitedReconnectExponentialBackoff.default : ReconnectExponentialBackoff

Equations

• LeanRedis.instInhabitedReconnectExponentialBackoff.default = { baseDelayMs := default, maxDelayMs := default, jitter := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedReconnectExponentialBackoff : Inhabited ReconnectExponentialBackoff

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprReconnectExponentialBackoff : Repr ReconnectExponentialBackoff

Equations

• LeanRedis.instReprReconnectExponentialBackoff = { reprPrec := LeanRedis.instReprReconnectExponentialBackoff.repr }

def LeanRedis.instReprReconnectExponentialBackoff.repr : ReconnectExponentialBackoff → Nat → Std.Format

Equations

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

inductive LeanRedis.ReconnectStrategy : Type

• disabled : ReconnectStrategy
• fixedInterval (delayMs : UInt32) (maxAttempts? : Option Nat := none) : ReconnectStrategy
• exponentialBackoff (config : ReconnectExponentialBackoff := { }) (maxAttempts? : Option Nat := none) : ReconnectStrategy

@[implicit_reducible]

instance LeanRedis.instBEqReconnectStrategy : BEq ReconnectStrategy

Equations

• LeanRedis.instBEqReconnectStrategy = { beq := LeanRedis.instBEqReconnectStrategy.beq }

def LeanRedis.instBEqReconnectStrategy.beq : ReconnectStrategy → ReconnectStrategy → Bool

Equations

• LeanRedis.instBEqReconnectStrategy.beq LeanRedis.ReconnectStrategy.disabled LeanRedis.ReconnectStrategy.disabled = true
• LeanRedis.instBEqReconnectStrategy.beq (LeanRedis.ReconnectStrategy.fixedInterval a a_1) (LeanRedis.ReconnectStrategy.fixedInterval b b_1) = (a == b && a_1 == b_1)
• LeanRedis.instBEqReconnectStrategy.beq (LeanRedis.ReconnectStrategy.exponentialBackoff a a_1) (LeanRedis.ReconnectStrategy.exponentialBackoff b b_1) = (a == b && a_1 == b_1)
• LeanRedis.instBEqReconnectStrategy.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedReconnectStrategy.default : ReconnectStrategy

Equations

• LeanRedis.instInhabitedReconnectStrategy.default = LeanRedis.ReconnectStrategy.disabled

@[implicit_reducible]

instance LeanRedis.instInhabitedReconnectStrategy : Inhabited ReconnectStrategy

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprReconnectStrategy : Repr ReconnectStrategy

Equations

• LeanRedis.instReprReconnectStrategy = { reprPrec := LeanRedis.instReprReconnectStrategy.repr }

def LeanRedis.instReprReconnectStrategy.repr : ReconnectStrategy → Nat → Std.Format

Equations

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

inductive LeanRedis.ProtocolPreference : Type

• auto : ProtocolPreference
• resp2 : ProtocolPreference
• resp3 : ProtocolPreference

def LeanRedis.instBEqProtocolPreference.beq : ProtocolPreference → ProtocolPreference → Bool

Equations

• LeanRedis.instBEqProtocolPreference.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance LeanRedis.instBEqProtocolPreference : BEq ProtocolPreference

Equations

• LeanRedis.instBEqProtocolPreference = { beq := LeanRedis.instBEqProtocolPreference.beq }

@[implicit_reducible]

instance LeanRedis.instInhabitedProtocolPreference : Inhabited ProtocolPreference

Equations

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

def LeanRedis.instInhabitedProtocolPreference.default : ProtocolPreference

Equations

• LeanRedis.instInhabitedProtocolPreference.default = LeanRedis.ProtocolPreference.auto

@[implicit_reducible]

instance LeanRedis.instReprProtocolPreference : Repr ProtocolPreference

Equations

• LeanRedis.instReprProtocolPreference = { reprPrec := LeanRedis.instReprProtocolPreference.repr }

def LeanRedis.instReprProtocolPreference.repr : ProtocolPreference → Nat → Std.Format

Equations

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

structure LeanRedis.AuthConfig : Type

• username? : Option String
• password : Redacted

@[implicit_reducible]

instance LeanRedis.instBEqAuthConfig : BEq AuthConfig

Equations

• LeanRedis.instBEqAuthConfig = { beq := LeanRedis.instBEqAuthConfig.beq }

def LeanRedis.instBEqAuthConfig.beq : AuthConfig → AuthConfig → Bool

Equations

• LeanRedis.instBEqAuthConfig.beq { username? := a, password := a_1 } { username? := b, password := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqAuthConfig.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedAuthConfig.default : AuthConfig

Equations

• LeanRedis.instInhabitedAuthConfig.default = { username? := default, password := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedAuthConfig : Inhabited AuthConfig

Equations

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

def LeanRedis.instReprAuthConfig.repr : AuthConfig → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprAuthConfig : Repr AuthConfig

Equations

• LeanRedis.instReprAuthConfig = { reprPrec := LeanRedis.instReprAuthConfig.repr }

structure LeanRedis.TimeoutConfig : Type

• connectMs? : Option UInt32
• responseMs? : Option UInt32

@[implicit_reducible]

instance LeanRedis.instBEqTimeoutConfig : BEq TimeoutConfig

Equations

• LeanRedis.instBEqTimeoutConfig = { beq := LeanRedis.instBEqTimeoutConfig.beq }

def LeanRedis.instBEqTimeoutConfig.beq : TimeoutConfig → TimeoutConfig → Bool

Equations

• LeanRedis.instBEqTimeoutConfig.beq { connectMs? := a, responseMs? := a_1 } { connectMs? := b, responseMs? := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqTimeoutConfig.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedTimeoutConfig.default : TimeoutConfig

Equations

• LeanRedis.instInhabitedTimeoutConfig.default = { connectMs? := default, responseMs? := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedTimeoutConfig : Inhabited TimeoutConfig

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprTimeoutConfig : Repr TimeoutConfig

Equations

• LeanRedis.instReprTimeoutConfig = { reprPrec := LeanRedis.instReprTimeoutConfig.repr }

def LeanRedis.instReprTimeoutConfig.repr : TimeoutConfig → Nat → Std.Format

Equations

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

structure LeanRedis.Config : Type

• endpoint : Transport.Endpoint
• auth? : Option AuthConfig
• database? : Option UInt32
• protocolPreference : ProtocolPreference
• clientName? : Option String
• timeouts : TimeoutConfig
• reconnectStrategy : ReconnectStrategy

def LeanRedis.instBEqConfig.beq : Config → Config → Bool

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.instBEqConfig.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqConfig : BEq Config

Equations

• LeanRedis.instBEqConfig = { beq := LeanRedis.instBEqConfig.beq }

def LeanRedis.instReprConfig.repr : Config → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprConfig : Repr Config

Equations

• LeanRedis.instReprConfig = { reprPrec := LeanRedis.instReprConfig.repr }

@[implicit_reducible]

instance LeanRedis.instInhabitedConfig : Inhabited Config

Equations

• LeanRedis.instInhabitedConfig = { default := { endpoint := { host := "", port := 0 } } }