inductive LeanRedis.Protocol.HelloOutcome : Type

• negotiated (version : Version) : HelloOutcome
• fallbackToResp2 : HelloOutcome

def LeanRedis.Protocol.instBEqHelloOutcome.beq : HelloOutcome → HelloOutcome → Bool

Equations

• LeanRedis.Protocol.instBEqHelloOutcome.beq (LeanRedis.Protocol.HelloOutcome.negotiated a) (LeanRedis.Protocol.HelloOutcome.negotiated b) = (a == b)
• LeanRedis.Protocol.instBEqHelloOutcome.beq LeanRedis.Protocol.HelloOutcome.fallbackToResp2 LeanRedis.Protocol.HelloOutcome.fallbackToResp2 = true
• LeanRedis.Protocol.instBEqHelloOutcome.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqHelloOutcome : BEq HelloOutcome

Equations

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

def LeanRedis.Protocol.instInhabitedHelloOutcome.default : HelloOutcome

Equations

• LeanRedis.Protocol.instInhabitedHelloOutcome.default = LeanRedis.Protocol.HelloOutcome.negotiated default

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedHelloOutcome : Inhabited HelloOutcome

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instReprHelloOutcome : Repr HelloOutcome

Equations

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

def LeanRedis.Protocol.instReprHelloOutcome.repr : HelloOutcome → Nat → Std.Format

Equations

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

inductive LeanRedis.Protocol.BootstrapStep : Type

• auth (request : CommandRequest) : BootstrapStep
• hello (request : CommandRequest) : BootstrapStep
• select (request : CommandRequest) : BootstrapStep

def LeanRedis.Protocol.instBEqBootstrapStep.beq : BootstrapStep → BootstrapStep → Bool

Equations

• LeanRedis.Protocol.instBEqBootstrapStep.beq (LeanRedis.Protocol.BootstrapStep.auth a) (LeanRedis.Protocol.BootstrapStep.auth b) = (a == b)
• LeanRedis.Protocol.instBEqBootstrapStep.beq (LeanRedis.Protocol.BootstrapStep.hello a) (LeanRedis.Protocol.BootstrapStep.hello b) = (a == b)
• LeanRedis.Protocol.instBEqBootstrapStep.beq (LeanRedis.Protocol.BootstrapStep.select a) (LeanRedis.Protocol.BootstrapStep.select b) = (a == b)
• LeanRedis.Protocol.instBEqBootstrapStep.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.Protocol.instBEqBootstrapStep : BEq BootstrapStep

Equations

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

@[implicit_reducible]

instance LeanRedis.Protocol.instInhabitedBootstrapStep : Inhabited BootstrapStep

Equations

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

def LeanRedis.Protocol.instInhabitedBootstrapStep.default : BootstrapStep

Equations

• LeanRedis.Protocol.instInhabitedBootstrapStep.default = LeanRedis.Protocol.BootstrapStep.auth default

def LeanRedis.Protocol.BootstrapStep.request : BootstrapStep → CommandRequest

Equations

• (LeanRedis.Protocol.BootstrapStep.auth request).request = request
• (LeanRedis.Protocol.BootstrapStep.hello request).request = request
• (LeanRedis.Protocol.BootstrapStep.select request).request = request

def LeanRedis.Protocol.preferredVersion (preference : ProtocolPreference) : Version

Equations

• LeanRedis.Protocol.preferredVersion LeanRedis.ProtocolPreference.resp2 = LeanRedis.Protocol.Version.resp2
• LeanRedis.Protocol.preferredVersion LeanRedis.ProtocolPreference.resp3 = LeanRedis.Protocol.Version.resp3
• LeanRedis.Protocol.preferredVersion LeanRedis.ProtocolPreference.auto = LeanRedis.Protocol.Version.resp3

def LeanRedis.Protocol.helloCommand : CommandRequest

Equations

• LeanRedis.Protocol.helloCommand = { name := "HELLO", args := #["3".toUTF8] }

def LeanRedis.Protocol.authCommand (auth : AuthConfig) : CommandRequest

Equations

• LeanRedis.Protocol.authCommand auth = LeanRedis.CommandRequest.auth auth

def LeanRedis.Protocol.selectCommand (database : UInt32) : CommandRequest

Equations

• LeanRedis.Protocol.selectCommand database = { name := "SELECT", args := #[(toString database).toUTF8] }

def LeanRedis.Protocol.bootstrapPlan (config : Config) : Array BootstrapStep

Equations

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

def LeanRedis.Protocol.bootstrapRequests (config : Config) : Array CommandRequest

Equations

• LeanRedis.Protocol.bootstrapRequests config = Array.map LeanRedis.Protocol.BootstrapStep.request (LeanRedis.Protocol.bootstrapPlan config)

def LeanRedis.Protocol.decideHelloOutcome (reply : Resp.Value) : Option HelloOutcome

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.Protocol.decideHelloOutcome (LeanRedis.Protocol.Resp.Value.simpleError message) = some LeanRedis.Protocol.HelloOutcome.fallbackToResp2
• LeanRedis.Protocol.decideHelloOutcome (LeanRedis.Protocol.Resp.Value.simpleString "OK") = some (LeanRedis.Protocol.HelloOutcome.negotiated LeanRedis.Protocol.Version.resp2)
• LeanRedis.Protocol.decideHelloOutcome reply = none

def LeanRedis.Protocol.protocolAfterHello (preference : ProtocolPreference) (reply : Resp.Value) : Option Version

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.Protocol.protocolAfterHello LeanRedis.ProtocolPreference.resp2 reply = some LeanRedis.Protocol.Version.resp2

def LeanRedis.Protocol.initialProtocol (preference : ProtocolPreference) : Version

Equations

• LeanRedis.Protocol.initialProtocol LeanRedis.ProtocolPreference.resp2 = LeanRedis.Protocol.Version.resp2
• LeanRedis.Protocol.initialProtocol LeanRedis.ProtocolPreference.resp3 = LeanRedis.Protocol.Version.resp2
• LeanRedis.Protocol.initialProtocol LeanRedis.ProtocolPreference.auto = LeanRedis.Protocol.Version.resp2

def LeanRedis.Protocol.applyHelloReply (state : State) (preference : ProtocolPreference) (reply : Resp.Value) : Option State

Equations

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

def LeanRedis.Protocol.markBootstrapReady (state : State) (protocol : Version) (database? : Option UInt32) : State

Equations

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

def LeanRedis.Protocol.applyBootstrapReply (state : State) (preference : ProtocolPreference) (step : BootstrapStep) (reply : Resp.Value) : Option State

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.Protocol.applyBootstrapReply state preference (LeanRedis.Protocol.BootstrapStep.auth request) reply = none
• LeanRedis.Protocol.applyBootstrapReply state preference (LeanRedis.Protocol.BootstrapStep.hello request) reply = LeanRedis.Protocol.applyHelloReply state preference reply
• LeanRedis.Protocol.applyBootstrapReply state preference (LeanRedis.Protocol.BootstrapStep.select request) reply = none

def LeanRedis.Protocol.bootstrapStateAfterStep (state : State) (config : Config) (step : BootstrapStep) (reply : Resp.Value) : Option State

Equations

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

def LeanRedis.Protocol.bootstrapStateAfterReplies (config : Config) (replies : Array Resp.Value) : Option State

Equations

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

def LeanRedis.Protocol.bootstrapSucceeded (state : State) (preference : ProtocolPreference) (helloReply : Resp.Value) (database? : Option UInt32) : Option State

Equations

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