def LeanRedis.ReconnectStrategy.shouldAttempt (strategy : ReconnectStrategy) (attempt : Nat) : Bool

Equations

• LeanRedis.ReconnectStrategy.disabled.shouldAttempt attempt = false
• (LeanRedis.ReconnectStrategy.fixedInterval delayMs).shouldAttempt attempt = true
• (LeanRedis.ReconnectStrategy.fixedInterval delayMs (some maxAttempts)).shouldAttempt attempt = decide (attempt < maxAttempts)
• (LeanRedis.ReconnectStrategy.exponentialBackoff config).shouldAttempt attempt = true
• (LeanRedis.ReconnectStrategy.exponentialBackoff config (some maxAttempts)).shouldAttempt attempt = decide (attempt < maxAttempts)

def LeanRedis.ReconnectStrategy.delayMs (strategy : ReconnectStrategy) (attempt : Nat) : IO (Option UInt32)

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.ReconnectStrategy.disabled.delayMs attempt = if (!LeanRedis.ReconnectStrategy.disabled.shouldAttempt attempt) = true then pure none else pure none