inductive LeanRedis.Error : Type

• transport (message : String) : Error
• protocol (message : String) : Error
• server (message : String) : Error
• decode (message : String) : Error
• bootstrap (message : String) : Error
• unavailable (message : String) : Error

def LeanRedis.instBEqError.beq : Error → Error → Bool

Equations

• LeanRedis.instBEqError.beq (LeanRedis.Error.transport a) (LeanRedis.Error.transport b) = (a == b)
• LeanRedis.instBEqError.beq (LeanRedis.Error.protocol a) (LeanRedis.Error.protocol b) = (a == b)
• LeanRedis.instBEqError.beq (LeanRedis.Error.server a) (LeanRedis.Error.server b) = (a == b)
• LeanRedis.instBEqError.beq (LeanRedis.Error.decode a) (LeanRedis.Error.decode b) = (a == b)
• LeanRedis.instBEqError.beq (LeanRedis.Error.bootstrap a) (LeanRedis.Error.bootstrap b) = (a == b)
• LeanRedis.instBEqError.beq (LeanRedis.Error.unavailable a) (LeanRedis.Error.unavailable b) = (a == b)
• LeanRedis.instBEqError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqError : BEq Error

Equations

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

def LeanRedis.instInhabitedError.default : Error

Equations

• LeanRedis.instInhabitedError.default = LeanRedis.Error.transport default

@[implicit_reducible]

instance LeanRedis.instInhabitedError : Inhabited Error

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprError : Repr Error

Equations

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

def LeanRedis.instReprError.repr : Error → Nat → Std.Format

Equations

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

def LeanRedis.Error.isTransport : Error → Bool

Equations

• (LeanRedis.Error.transport message).isTransport = true
• x✝.isTransport = false

def LeanRedis.Error.message : Error → String

Equations

• (LeanRedis.Error.transport a).message = toString "transport error: " ++ toString a
• (LeanRedis.Error.protocol a).message = toString "protocol error: " ++ toString a
• (LeanRedis.Error.server a).message = toString "server error: " ++ toString a
• (LeanRedis.Error.decode a).message = toString "decode error: " ++ toString a
• (LeanRedis.Error.bootstrap a).message = toString "bootstrap error: " ++ toString a
• (LeanRedis.Error.unavailable a).message = toString "unavailable: " ++ toString a

@[implicit_reducible]

instance LeanRedis.instMonadLiftExceptErrorIO : MonadLift (Except Error) IO

Equations

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

def LeanRedis.Error.raise {α : Type} (err : Error) : IO α

Equations

• err.raise = throw (IO.userError err.message)

def LeanRedis.Error.isTransportIOError (err : IO.Error) : Bool

Equations

• LeanRedis.Error.isTransportIOError (IO.Error.userError msg) = msg.startsWith "transport error:"
• LeanRedis.Error.isTransportIOError err = false