structure LeanRedis.ZScanOptions : Type

• match? : Option String
• count? : Option UInt64

@[implicit_reducible]

instance LeanRedis.instBEqZScanOptions : BEq ZScanOptions

Equations

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

def LeanRedis.instBEqZScanOptions.beq : ZScanOptions → ZScanOptions → Bool

Equations

• LeanRedis.instBEqZScanOptions.beq { match? := a, count? := a_1 } { match? := b, count? := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqZScanOptions.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedZScanOptions.default : ZScanOptions

Equations

• LeanRedis.instInhabitedZScanOptions.default = { match? := default, count? := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedZScanOptions : Inhabited ZScanOptions

Equations

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

def LeanRedis.instReprZScanOptions.repr : ZScanOptions → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprZScanOptions : Repr ZScanOptions

Equations

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

def LeanRedis.CommandRequest.zScanArgs (options : ZScanOptions) : Array ByteArray

Equations

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

def LeanRedis.CommandRequest.sortedSetEntryArgs (entries : Array SortedSetEntry) : Array ByteArray

Equations

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

def LeanRedis.CommandRequest.zAdd (key : String) (entries : Array SortedSetEntry) : CommandRequest

ZADD key score member [score member ...]

Equations

• LeanRedis.CommandRequest.zAdd key entries = { name := "ZADD", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.sortedSetEntryArgs entries }

def LeanRedis.CommandRequest.zRem (key : String) (members : Array String) : CommandRequest

ZREM key member [member ...]

Equations

• LeanRedis.CommandRequest.zRem key members = { name := "ZREM", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args members }

def LeanRedis.CommandRequest.zCard (key : String) : CommandRequest

ZCARD key

Equations

• LeanRedis.CommandRequest.zCard key = { name := "ZCARD", args := LeanRedis.CommandRequest.utf8Args #[key] }

def LeanRedis.CommandRequest.zScore (key member : String) : CommandRequest

ZSCORE key member

Equations

• LeanRedis.CommandRequest.zScore key member = { name := "ZSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, member] }

def LeanRedis.CommandRequest.zMScore (key : String) (members : Array String) : CommandRequest

ZMSCORE key member [member ...]

Equations

• LeanRedis.CommandRequest.zMScore key members = { name := "ZMSCORE", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args members }

def LeanRedis.CommandRequest.zRank (key member : String) : CommandRequest

ZRANK key member

Equations

• LeanRedis.CommandRequest.zRank key member = { name := "ZRANK", args := LeanRedis.CommandRequest.utf8Args #[key, member] }

def LeanRedis.CommandRequest.zRevRank (key member : String) : CommandRequest

ZREVRANK key member

Equations

• LeanRedis.CommandRequest.zRevRank key member = { name := "ZREVRANK", args := LeanRedis.CommandRequest.utf8Args #[key, member] }

def LeanRedis.CommandRequest.zRange (key : String) (start stop : Int) : CommandRequest

ZRANGE key start stop [BYSCORE | BYLEX] [REV] [LIMIT offset count] [WITHSCORES]

Equations

• LeanRedis.CommandRequest.zRange key start stop = { name := "ZRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop] }

def LeanRedis.CommandRequest.zRangeWithScores (key : String) (start stop : Int) : CommandRequest

ZRANGE key start stop WITHSCORES

Equations

• LeanRedis.CommandRequest.zRangeWithScores key start stop = { name := "ZRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop, "WITHSCORES"] }

def LeanRedis.CommandRequest.zRevRange (key : String) (start stop : Int) : CommandRequest

ZREVRANGE key start stop [WITHSCORES]

Equations

• LeanRedis.CommandRequest.zRevRange key start stop = { name := "ZREVRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop] }

def LeanRedis.CommandRequest.zRevRangeWithScores (key : String) (start stop : Int) : CommandRequest

ZREVRANGE key start stop WITHSCORES

Equations

• LeanRedis.CommandRequest.zRevRangeWithScores key start stop = { name := "ZREVRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop, "WITHSCORES"] }

def LeanRedis.CommandRequest.zRangeByScore (key min max : String) : CommandRequest

ZRANGEBYSCORE key min max [WITHSCORES] [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRangeByScore key min max = { name := "ZRANGEBYSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zRangeByScoreWithScores (key min max : String) : CommandRequest

ZRANGEBYSCORE key min max WITHSCORES [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRangeByScoreWithScores key min max = { name := "ZRANGEBYSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, min, max, "WITHSCORES"] }

def LeanRedis.CommandRequest.zRevRangeByScore (key max min : String) : CommandRequest

ZREVRANGEBYSCORE key max min [WITHSCORES] [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRevRangeByScore key max min = { name := "ZREVRANGEBYSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, max, min] }

def LeanRedis.CommandRequest.zRevRangeByScoreWithScores (key max min : String) : CommandRequest

ZREVRANGEBYSCORE key max min WITHSCORES [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRevRangeByScoreWithScores key max min = { name := "ZREVRANGEBYSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, max, min, "WITHSCORES"] }

def LeanRedis.CommandRequest.zRangeByLex (key min max : String) : CommandRequest

ZRANGEBYLEX key min max [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRangeByLex key min max = { name := "ZRANGEBYLEX", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zRevRangeByLex (key max min : String) : CommandRequest

ZREVRANGEBYLEX key max min [LIMIT offset count]

Equations

• LeanRedis.CommandRequest.zRevRangeByLex key max min = { name := "ZREVRANGEBYLEX", args := LeanRedis.CommandRequest.utf8Args #[key, max, min] }

def LeanRedis.CommandRequest.zCount (key min max : String) : CommandRequest

ZCOUNT key min max

Equations

• LeanRedis.CommandRequest.zCount key min max = { name := "ZCOUNT", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zLexCount (key min max : String) : CommandRequest

ZLEXCOUNT key min max

Equations

• LeanRedis.CommandRequest.zLexCount key min max = { name := "ZLEXCOUNT", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zRemRangeByRank (key : String) (start stop : Int) : CommandRequest

ZREMRANGEBYRANK key start stop

Equations

• LeanRedis.CommandRequest.zRemRangeByRank key start stop = { name := "ZREMRANGEBYRANK", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop] }

def LeanRedis.CommandRequest.zRemRangeByScore (key min max : String) : CommandRequest

ZREMRANGEBYSCORE key min max

Equations

• LeanRedis.CommandRequest.zRemRangeByScore key min max = { name := "ZREMRANGEBYSCORE", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zRemRangeByLex (key min max : String) : CommandRequest

ZREMRANGEBYLEX key min max

Equations

• LeanRedis.CommandRequest.zRemRangeByLex key min max = { name := "ZREMRANGEBYLEX", args := LeanRedis.CommandRequest.utf8Args #[key, min, max] }

def LeanRedis.CommandRequest.zIncrBy (key increment member : String) : CommandRequest

ZINCRBY key increment member

Equations

• LeanRedis.CommandRequest.zIncrBy key increment member = { name := "ZINCRBY", args := LeanRedis.CommandRequest.utf8Args #[key, increment, member] }

def LeanRedis.CommandRequest.zRandMember (key : String) : CommandRequest

ZRANDMEMBER key [count [WITHSCORES]]

Equations

• LeanRedis.CommandRequest.zRandMember key = { name := "ZRANDMEMBER", args := LeanRedis.CommandRequest.utf8Args #[key] }

def LeanRedis.CommandRequest.zRandMembers (key : String) (count : Int) : CommandRequest

ZRANDMEMBER key count

Equations

• LeanRedis.CommandRequest.zRandMembers key count = { name := "ZRANDMEMBER", args := LeanRedis.CommandRequest.utf8Args #[key, toString count] }

def LeanRedis.CommandRequest.zRandMembersWithScores (key : String) (count : Int) : CommandRequest

ZRANDMEMBER key count WITHSCORES

Equations

• LeanRedis.CommandRequest.zRandMembersWithScores key count = { name := "ZRANDMEMBER", args := LeanRedis.CommandRequest.utf8Args #[key, toString count, "WITHSCORES"] }

def LeanRedis.CommandRequest.zDiff (keys : Array String) : CommandRequest

ZDIFF numkeys key [key ...]

Equations

• LeanRedis.CommandRequest.zDiff keys = { name := "ZDIFF", args := LeanRedis.CommandRequest.utf8Args #[toString keys.size] ++ LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.zDiffStore (destination : String) (keys : Array String) : CommandRequest

ZDIFFSTORE destination numkeys key [key ...]

Equations

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

def LeanRedis.CommandRequest.zInter (keys : Array String) : CommandRequest

ZINTER numkeys key [key ...]

Equations

• LeanRedis.CommandRequest.zInter keys = { name := "ZINTER", args := LeanRedis.CommandRequest.utf8Args #[toString keys.size] ++ LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.zInterCard (keys : Array String) : CommandRequest

ZINTERCARD numkeys key [key ...]

Equations

• LeanRedis.CommandRequest.zInterCard keys = { name := "ZINTERCARD", args := LeanRedis.CommandRequest.utf8Args #[toString keys.size] ++ LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.zInterStore (destination : String) (keys : Array String) : CommandRequest

ZINTERSTORE destination numkeys key [key ...]

Equations

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

def LeanRedis.CommandRequest.zUnion (keys : Array String) : CommandRequest

ZUNION numkeys key [key ...]

Equations

• LeanRedis.CommandRequest.zUnion keys = { name := "ZUNION", args := LeanRedis.CommandRequest.utf8Args #[toString keys.size] ++ LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.zUnionStore (destination : String) (keys : Array String) : CommandRequest

ZUNIONSTORE destination numkeys key [key ...]

Equations

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

def LeanRedis.CommandRequest.zScan (key : String) (cursor : UInt64) (options : ZScanOptions := { }) : CommandRequest

ZSCAN key cursor [MATCH pattern] [COUNT count]

Equations

• LeanRedis.CommandRequest.zScan key cursor options = { name := "ZSCAN", args := LeanRedis.CommandRequest.utf8Args #[key, toString cursor] ++ LeanRedis.CommandRequest.zScanArgs options }

def LeanRedis.Command.zAdd (key : String) (entries : Array SortedSetEntry) : Command Int

Equations

• LeanRedis.Command.zAdd key entries = { request := LeanRedis.CommandRequest.zAdd key entries, decode := LeanRedis.expectInteger "ZADD" }

def LeanRedis.Command.zRem (key : String) (members : Array String) : Command Int

Equations

• LeanRedis.Command.zRem key members = { request := LeanRedis.CommandRequest.zRem key members, decode := LeanRedis.expectInteger "ZREM" }

def LeanRedis.Command.zCard (key : String) : Command Int

Equations

• LeanRedis.Command.zCard key = { request := LeanRedis.CommandRequest.zCard key, decode := LeanRedis.expectInteger "ZCARD" }

def LeanRedis.Command.zScore (key member : String) : Command (Option String)

Equations

• LeanRedis.Command.zScore key member = { request := LeanRedis.CommandRequest.zScore key member, decode := LeanRedis.expectOptionalString "ZSCORE" }

def LeanRedis.Command.zMScore (key : String) (members : Array String) : Command (Array (Option String))

Equations

• LeanRedis.Command.zMScore key members = { request := LeanRedis.CommandRequest.zMScore key members, decode := LeanRedis.expectStringArray "ZMSCORE" }

def LeanRedis.Command.zRank (key member : String) : Command (Option Int)

Equations

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

def LeanRedis.Command.zRevRank (key member : String) : Command (Option Int)

Equations

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

def LeanRedis.Command.zRange (key : String) (start stop : Int) : Command (Array String)

Equations

• LeanRedis.Command.zRange key start stop = { request := LeanRedis.CommandRequest.zRange key start stop, decode := LeanRedis.expectPlainStringArray "ZRANGE" }

def LeanRedis.Command.zRangeWithScores (key : String) (start stop : Int) : Command (Array SortedSetEntry)

Equations

• LeanRedis.Command.zRangeWithScores key start stop = { request := LeanRedis.CommandRequest.zRangeWithScores key start stop, decode := LeanRedis.expectSortedSetEntries "ZRANGE" }

def LeanRedis.Command.zRevRange (key : String) (start stop : Int) : Command (Array String)

Equations

• LeanRedis.Command.zRevRange key start stop = { request := LeanRedis.CommandRequest.zRevRange key start stop, decode := LeanRedis.expectPlainStringArray "ZREVRANGE" }

def LeanRedis.Command.zRevRangeWithScores (key : String) (start stop : Int) : Command (Array SortedSetEntry)

Equations

• LeanRedis.Command.zRevRangeWithScores key start stop = { request := LeanRedis.CommandRequest.zRevRangeWithScores key start stop, decode := LeanRedis.expectSortedSetEntries "ZREVRANGE" }

def LeanRedis.Command.zRangeByScore (key min max : String) : Command (Array String)

Equations

• LeanRedis.Command.zRangeByScore key min max = { request := LeanRedis.CommandRequest.zRangeByScore key min max, decode := LeanRedis.expectPlainStringArray "ZRANGEBYSCORE" }

def LeanRedis.Command.zRangeByScoreWithScores (key min max : String) : Command (Array SortedSetEntry)

Equations

• LeanRedis.Command.zRangeByScoreWithScores key min max = { request := LeanRedis.CommandRequest.zRangeByScoreWithScores key min max, decode := LeanRedis.expectSortedSetEntries "ZRANGEBYSCORE" }

def LeanRedis.Command.zRevRangeByScore (key max min : String) : Command (Array String)

Equations

• LeanRedis.Command.zRevRangeByScore key max min = { request := LeanRedis.CommandRequest.zRevRangeByScore key max min, decode := LeanRedis.expectPlainStringArray "ZREVRANGEBYSCORE" }

def LeanRedis.Command.zRevRangeByScoreWithScores (key max min : String) : Command (Array SortedSetEntry)

Equations

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

def LeanRedis.Command.zRangeByLex (key min max : String) : Command (Array String)

Equations

• LeanRedis.Command.zRangeByLex key min max = { request := LeanRedis.CommandRequest.zRangeByLex key min max, decode := LeanRedis.expectPlainStringArray "ZRANGEBYLEX" }

def LeanRedis.Command.zRevRangeByLex (key max min : String) : Command (Array String)

Equations

• LeanRedis.Command.zRevRangeByLex key max min = { request := LeanRedis.CommandRequest.zRevRangeByLex key max min, decode := LeanRedis.expectPlainStringArray "ZREVRANGEBYLEX" }

def LeanRedis.Command.zCount (key min max : String) : Command Int

Equations

• LeanRedis.Command.zCount key min max = { request := LeanRedis.CommandRequest.zCount key min max, decode := LeanRedis.expectInteger "ZCOUNT" }

def LeanRedis.Command.zLexCount (key min max : String) : Command Int

Equations

• LeanRedis.Command.zLexCount key min max = { request := LeanRedis.CommandRequest.zLexCount key min max, decode := LeanRedis.expectInteger "ZLEXCOUNT" }

def LeanRedis.Command.zRemRangeByRank (key : String) (start stop : Int) : Command Int

Equations

• LeanRedis.Command.zRemRangeByRank key start stop = { request := LeanRedis.CommandRequest.zRemRangeByRank key start stop, decode := LeanRedis.expectInteger "ZREMRANGEBYRANK" }

def LeanRedis.Command.zRemRangeByScore (key min max : String) : Command Int

Equations

• LeanRedis.Command.zRemRangeByScore key min max = { request := LeanRedis.CommandRequest.zRemRangeByScore key min max, decode := LeanRedis.expectInteger "ZREMRANGEBYSCORE" }

def LeanRedis.Command.zRemRangeByLex (key min max : String) : Command Int

Equations

• LeanRedis.Command.zRemRangeByLex key min max = { request := LeanRedis.CommandRequest.zRemRangeByLex key min max, decode := LeanRedis.expectInteger "ZREMRANGEBYLEX" }

def LeanRedis.Command.zIncrBy (key increment member : String) : Command String

Equations

• LeanRedis.Command.zIncrBy key increment member = { request := LeanRedis.CommandRequest.zIncrBy key increment member, decode := LeanRedis.expectString "ZINCRBY" }

def LeanRedis.Command.zRandMember (key : String) : Command (Option String)

Equations

• LeanRedis.Command.zRandMember key = { request := LeanRedis.CommandRequest.zRandMember key, decode := LeanRedis.expectOptionalString "ZRANDMEMBER" }

def LeanRedis.Command.zRandMembers (key : String) (count : Int) : Command (Array String)

Equations

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

def LeanRedis.Command.zRandMembersWithScores (key : String) (count : Int) : Command (Array SortedSetEntry)

Equations

• LeanRedis.Command.zRandMembersWithScores key count = { request := LeanRedis.CommandRequest.zRandMembersWithScores key count, decode := LeanRedis.expectSortedSetEntries "ZRANDMEMBER" }

def LeanRedis.Command.zDiff (keys : Array String) : Command (Array String)

Equations

• LeanRedis.Command.zDiff keys = { request := LeanRedis.CommandRequest.zDiff keys, decode := LeanRedis.expectPlainStringArray "ZDIFF" }

def LeanRedis.Command.zDiffStore (destination : String) (keys : Array String) : Command Int

Equations

• LeanRedis.Command.zDiffStore destination keys = { request := LeanRedis.CommandRequest.zDiffStore destination keys, decode := LeanRedis.expectInteger "ZDIFFSTORE" }

def LeanRedis.Command.zInter (keys : Array String) : Command (Array String)

Equations

• LeanRedis.Command.zInter keys = { request := LeanRedis.CommandRequest.zInter keys, decode := LeanRedis.expectPlainStringArray "ZINTER" }

def LeanRedis.Command.zInterCard (keys : Array String) : Command Int

Equations

• LeanRedis.Command.zInterCard keys = { request := LeanRedis.CommandRequest.zInterCard keys, decode := LeanRedis.expectInteger "ZINTERCARD" }

def LeanRedis.Command.zInterStore (destination : String) (keys : Array String) : Command Int

Equations

• LeanRedis.Command.zInterStore destination keys = { request := LeanRedis.CommandRequest.zInterStore destination keys, decode := LeanRedis.expectInteger "ZINTERSTORE" }

def LeanRedis.Command.zUnion (keys : Array String) : Command (Array String)

Equations

• LeanRedis.Command.zUnion keys = { request := LeanRedis.CommandRequest.zUnion keys, decode := LeanRedis.expectPlainStringArray "ZUNION" }

def LeanRedis.Command.zUnionStore (destination : String) (keys : Array String) : Command Int

Equations

• LeanRedis.Command.zUnionStore destination keys = { request := LeanRedis.CommandRequest.zUnionStore destination keys, decode := LeanRedis.expectInteger "ZUNIONSTORE" }

def LeanRedis.Command.zScan (key : String) (cursor : UInt64) (options : ZScanOptions := { }) : Command SortedSetScanResult

Equations

• LeanRedis.Command.zScan key cursor options = { request := LeanRedis.CommandRequest.zScan key cursor options, decode := LeanRedis.expectSortedSetScanResult }