structure LeanRedis.CommandRequest : Type

• name : String
• args : Array ByteArray

@[implicit_reducible]

instance LeanRedis.instBEqCommandRequest : BEq CommandRequest

Equations

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

def LeanRedis.instBEqCommandRequest.beq : CommandRequest → CommandRequest → Bool

Equations

• LeanRedis.instBEqCommandRequest.beq { name := a, args := a_1 } { name := b, args := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqCommandRequest.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instInhabitedCommandRequest : Inhabited CommandRequest

Equations

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

def LeanRedis.instInhabitedCommandRequest.default : CommandRequest

Equations

• LeanRedis.instInhabitedCommandRequest.default = { name := default, args := default }

def LeanRedis.CommandRequest.utf8Args (args : Array String) : Array ByteArray

Equations

• LeanRedis.CommandRequest.utf8Args args = Array.map String.toUTF8 args

structure LeanRedis.Command (α : Type) : Type

• request : CommandRequest
• decode : Protocol.Resp.Value → Except Error α

def LeanRedis.instInhabitedCommand.default {a✝ : Type} : Command a✝

Equations

• LeanRedis.instInhabitedCommand.default = { request := default, decode := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedCommand {a✝ : Type} : Inhabited (Command a✝)

Equations

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

structure LeanRedis.ScanResult : Type

• cursor : UInt64
• keys : Array String

def LeanRedis.instBEqScanResult.beq : ScanResult → ScanResult → Bool

Equations

• LeanRedis.instBEqScanResult.beq { cursor := a, keys := a_1 } { cursor := b, keys := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqScanResult.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqScanResult : BEq ScanResult

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedScanResult : Inhabited ScanResult

Equations

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

def LeanRedis.instInhabitedScanResult.default : ScanResult

Equations

• LeanRedis.instInhabitedScanResult.default = { cursor := default, keys := default }

def LeanRedis.instReprScanResult.repr : ScanResult → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprScanResult : Repr ScanResult

Equations

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

structure LeanRedis.HashScanResult : Type

• cursor : UInt64
• entries : Array (String × String)

@[implicit_reducible]

instance LeanRedis.instBEqHashScanResult : BEq HashScanResult

Equations

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

def LeanRedis.instBEqHashScanResult.beq : HashScanResult → HashScanResult → Bool

Equations

• LeanRedis.instBEqHashScanResult.beq { cursor := a, entries := a_1 } { cursor := b, entries := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqHashScanResult.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedHashScanResult.default : HashScanResult

Equations

• LeanRedis.instInhabitedHashScanResult.default = { cursor := default, entries := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedHashScanResult : Inhabited HashScanResult

Equations

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

def LeanRedis.instReprHashScanResult.repr : HashScanResult → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprHashScanResult : Repr HashScanResult

Equations

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

structure LeanRedis.SetScanResult : Type

• cursor : UInt64
• members : Array String

def LeanRedis.instBEqSetScanResult.beq : SetScanResult → SetScanResult → Bool

Equations

• LeanRedis.instBEqSetScanResult.beq { cursor := a, members := a_1 } { cursor := b, members := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqSetScanResult.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqSetScanResult : BEq SetScanResult

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedSetScanResult : Inhabited SetScanResult

Equations

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

def LeanRedis.instInhabitedSetScanResult.default : SetScanResult

Equations

• LeanRedis.instInhabitedSetScanResult.default = { cursor := default, members := default }

def LeanRedis.instReprSetScanResult.repr : SetScanResult → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprSetScanResult : Repr SetScanResult

Equations

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

structure LeanRedis.SortedSetEntry : Type

• score : String
• member : String

def LeanRedis.instBEqSortedSetEntry.beq : SortedSetEntry → SortedSetEntry → Bool

Equations

• LeanRedis.instBEqSortedSetEntry.beq { score := a, member := a_1 } { score := b, member := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqSortedSetEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqSortedSetEntry : BEq SortedSetEntry

Equations

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

def LeanRedis.instInhabitedSortedSetEntry.default : SortedSetEntry

Equations

• LeanRedis.instInhabitedSortedSetEntry.default = { score := default, member := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedSortedSetEntry : Inhabited SortedSetEntry

Equations

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

def LeanRedis.instReprSortedSetEntry.repr : SortedSetEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprSortedSetEntry : Repr SortedSetEntry

Equations

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

structure LeanRedis.SortedSetScanResult : Type

• cursor : UInt64
• entries : Array SortedSetEntry

def LeanRedis.instBEqSortedSetScanResult.beq : SortedSetScanResult → SortedSetScanResult → Bool

Equations

• LeanRedis.instBEqSortedSetScanResult.beq { cursor := a, entries := a_1 } { cursor := b, entries := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqSortedSetScanResult.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqSortedSetScanResult : BEq SortedSetScanResult

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedSortedSetScanResult : Inhabited SortedSetScanResult

Equations

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

def LeanRedis.instInhabitedSortedSetScanResult.default : SortedSetScanResult

Equations

• LeanRedis.instInhabitedSortedSetScanResult.default = { cursor := default, entries := default }

@[implicit_reducible]

instance LeanRedis.instReprSortedSetScanResult : Repr SortedSetScanResult

Equations

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

def LeanRedis.instReprSortedSetScanResult.repr : SortedSetScanResult → Nat → Std.Format

Equations

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