inductive LeanRedis.Protocol.SessionPhase : Type

• disconnected : SessionPhase
• bootstrapping : SessionPhase
• ready : SessionPhase
• failed : SessionPhase

def LeanRedis.Protocol.instBEqSessionPhase.beq : SessionPhase → SessionPhase → Bool

Equations

• LeanRedis.Protocol.instBEqSessionPhase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqSessionPhase : BEq SessionPhase

Equations

• LeanRedis.Protocol.instBEqSessionPhase = { beq := LeanRedis.Protocol.instBEqSessionPhase.beq }

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedSessionPhase : Inhabited SessionPhase

Equations

• LeanRedis.Protocol.instInhabitedSessionPhase = { default := LeanRedis.Protocol.instInhabitedSessionPhase.default }

def LeanRedis.Protocol.instInhabitedSessionPhase.default : SessionPhase

Equations

• LeanRedis.Protocol.instInhabitedSessionPhase.default = LeanRedis.Protocol.SessionPhase.disconnected

def LeanRedis.Protocol.instReprSessionPhase.repr : SessionPhase → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instReprSessionPhase : Repr SessionPhase

Equations

• LeanRedis.Protocol.instReprSessionPhase = { reprPrec := LeanRedis.Protocol.instReprSessionPhase.repr }

structure LeanRedis.Protocol.State : Type

• phase : SessionPhase
• protocol? : Option Version
• selectedDb? : Option UInt32
• lastReply? : Option Resp.Value

def LeanRedis.Protocol.instBEqState.beq : State → State → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqState : BEq State

Equations

• LeanRedis.Protocol.instBEqState = { beq := LeanRedis.Protocol.instBEqState.beq }

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedState : Inhabited State

Equations

• LeanRedis.Protocol.instInhabitedState = { default := LeanRedis.Protocol.instInhabitedState.default }

def LeanRedis.Protocol.instInhabitedState.default : State

Equations

• LeanRedis.Protocol.instInhabitedState.default = { phase := default, protocol? := default, selectedDb? := default, lastReply? := default }