structure LeanRedis.SScanOptions : Type

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

@[implicit_reducible]

instance LeanRedis.instBEqSScanOptions : BEq SScanOptions

Equations

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

def LeanRedis.instBEqSScanOptions.beq : SScanOptions → SScanOptions → Bool

Equations

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

def LeanRedis.instInhabitedSScanOptions.default : SScanOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedSScanOptions : Inhabited SScanOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprSScanOptions : Repr SScanOptions

Equations

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

def LeanRedis.instReprSScanOptions.repr : SScanOptions → Nat → Std.Format

Equations

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

def LeanRedis.CommandRequest.sScanArgs (options : SScanOptions) : Array ByteArray

Equations

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

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

SADD key member [member ...]

Equations

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

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

SREM key member [member ...]

Equations

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

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

SCARD key

Equations

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

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

SISMEMBER key member

Equations

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

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

SMISMEMBER key member [member ...]

Equations

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

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

SMEMBERS key

Equations

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

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

SPOP key [count]

Equations

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

def LeanRedis.CommandRequest.sPopCount (key : String) (count : UInt64) : CommandRequest

SPOP key count

Equations

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

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

SRANDMEMBER key [count]

Equations

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

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

SRANDMEMBER key count

Equations

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

def LeanRedis.CommandRequest.sMove (source destination member : String) : CommandRequest

SMOVE source destination member

Equations

• LeanRedis.CommandRequest.sMove source destination member = { name := "SMOVE", args := LeanRedis.CommandRequest.utf8Args #[source, destination, member] }

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

SDIFF key [key ...]

Equations

• LeanRedis.CommandRequest.sDiff keys = { name := "SDIFF", args := LeanRedis.CommandRequest.utf8Args keys }

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

SDIFFSTORE destination key [key ...]

Equations

• LeanRedis.CommandRequest.sDiffStore destination keys = { name := "SDIFFSTORE", args := LeanRedis.CommandRequest.utf8Args #[destination] ++ LeanRedis.CommandRequest.utf8Args keys }

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

SINTER key [key ...]

Equations

• LeanRedis.CommandRequest.sInter keys = { name := "SINTER", args := LeanRedis.CommandRequest.utf8Args keys }

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

SINTERCARD numkeys key [key ...]

Equations

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

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

SINTERSTORE destination key [key ...]

Equations

• LeanRedis.CommandRequest.sInterStore destination keys = { name := "SINTERSTORE", args := LeanRedis.CommandRequest.utf8Args #[destination] ++ LeanRedis.CommandRequest.utf8Args keys }

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

SUNION key [key ...]

Equations

• LeanRedis.CommandRequest.sUnion keys = { name := "SUNION", args := LeanRedis.CommandRequest.utf8Args keys }

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

SUNIONSTORE destination key [key ...]

Equations

• LeanRedis.CommandRequest.sUnionStore destination keys = { name := "SUNIONSTORE", args := LeanRedis.CommandRequest.utf8Args #[destination] ++ LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.sScan (key : String) (cursor : UInt64) (options : SScanOptions := { }) : CommandRequest

SSCAN key cursor [MATCH pattern] [COUNT count]

Equations

• LeanRedis.CommandRequest.sScan key cursor options = { name := "SSCAN", args := LeanRedis.CommandRequest.utf8Args #[key, toString cursor] ++ LeanRedis.CommandRequest.sScanArgs options }

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

Equations

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

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

Equations

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

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

Equations

• LeanRedis.Command.sCard key = { request := LeanRedis.CommandRequest.sCard key, decode := LeanRedis.expectInteger "SCARD" }

def LeanRedis.Command.sIsMember (key member : String) : Command Bool

Equations

• LeanRedis.Command.sIsMember key member = { request := LeanRedis.CommandRequest.sIsMember key member, decode := LeanRedis.expectBoolean "SISMEMBER" }

def LeanRedis.Command.sMIsMember (key : String) (members : Array String) : Command (Array Bool)

Equations

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

def LeanRedis.Command.sMembers (key : String) : Command (Array String)

Equations

• LeanRedis.Command.sMembers key = { request := LeanRedis.CommandRequest.sMembers key, decode := LeanRedis.expectPlainStringArray "SMEMBERS" }

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

Equations

• LeanRedis.Command.sPop key = { request := LeanRedis.CommandRequest.sPop key, decode := LeanRedis.expectOptionalString "SPOP" }

def LeanRedis.Command.sPopMany (key : String) (count : UInt64) : Command (Array String)

Equations

• LeanRedis.Command.sPopMany key count = { request := LeanRedis.CommandRequest.sPopCount key count, decode := LeanRedis.expectPlainStringArray "SPOP" }

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

Equations

• LeanRedis.Command.sRandMember key = { request := LeanRedis.CommandRequest.sRandMember key, decode := LeanRedis.expectOptionalString "SRANDMEMBER" }

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

Equations

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

def LeanRedis.Command.sMove (source destination member : String) : Command Bool

Equations

• LeanRedis.Command.sMove source destination member = { request := LeanRedis.CommandRequest.sMove source destination member, decode := LeanRedis.expectBoolean "SMOVE" }

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

Equations

• LeanRedis.Command.sDiff keys = { request := LeanRedis.CommandRequest.sDiff keys, decode := LeanRedis.expectPlainStringArray "SDIFF" }

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

Equations

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

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

Equations

• LeanRedis.Command.sInter keys = { request := LeanRedis.CommandRequest.sInter keys, decode := LeanRedis.expectPlainStringArray "SINTER" }

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

Equations

• LeanRedis.Command.sInterCard keys = { request := LeanRedis.CommandRequest.sInterCard keys, decode := LeanRedis.expectInteger "SINTERCARD" }

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

Equations

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

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

Equations

• LeanRedis.Command.sUnion keys = { request := LeanRedis.CommandRequest.sUnion keys, decode := LeanRedis.expectPlainStringArray "SUNION" }

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

Equations

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

def LeanRedis.Command.sScan (key : String) (cursor : UInt64) (options : SScanOptions := { }) : Command SetScanResult

Equations

• LeanRedis.Command.sScan key cursor options = { request := LeanRedis.CommandRequest.sScan key cursor options, decode := LeanRedis.expectSetScanResult }