structure LeanRedis.HScanOptions : Type

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

@[implicit_reducible]

instance LeanRedis.instBEqHScanOptions : BEq HScanOptions

Equations

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

def LeanRedis.instBEqHScanOptions.beq : HScanOptions → HScanOptions → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedHScanOptions : Inhabited HScanOptions

Equations

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

def LeanRedis.instInhabitedHScanOptions.default : HScanOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprHScanOptions : Repr HScanOptions

Equations

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

def LeanRedis.instReprHScanOptions.repr : HScanOptions → Nat → Std.Format

Equations

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

def LeanRedis.CommandRequest.hScanArgs (options : HScanOptions) : Array ByteArray

Equations

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

def LeanRedis.CommandRequest.hGet (key field : String) : CommandRequest

HGET key field

Equations

• LeanRedis.CommandRequest.hGet key field = { name := "HGET", args := LeanRedis.CommandRequest.utf8Args #[key, field] }

def LeanRedis.CommandRequest.hSet (key : String) (entries : Array (String × String)) : CommandRequest

HSET key field value [field value ...]

Equations

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

def LeanRedis.CommandRequest.hMGet (key : String) (fields : Array String) : CommandRequest

HMGET key field [field ...]

Equations

• LeanRedis.CommandRequest.hMGet key fields = { name := "HMGET", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args fields }

def LeanRedis.CommandRequest.hMSet (key : String) (entries : Array (String × String)) : CommandRequest

HMSET key field value [field value ...]

Equations

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

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

HGETALL key

Equations

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

def LeanRedis.CommandRequest.hDel (key : String) (fields : Array String) : CommandRequest

HDEL key field [field ...]

Equations

• LeanRedis.CommandRequest.hDel key fields = { name := "HDEL", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args fields }

def LeanRedis.CommandRequest.hExists (key field : String) : CommandRequest

HEXISTS key field

Equations

• LeanRedis.CommandRequest.hExists key field = { name := "HEXISTS", args := LeanRedis.CommandRequest.utf8Args #[key, field] }

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

HLEN key

Equations

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

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

HKEYS key

Equations

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

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

HVALS key

Equations

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

def LeanRedis.CommandRequest.hStrLen (key field : String) : CommandRequest

HSTRLEN key field

Equations

• LeanRedis.CommandRequest.hStrLen key field = { name := "HSTRLEN", args := LeanRedis.CommandRequest.utf8Args #[key, field] }

def LeanRedis.CommandRequest.hIncrBy (key field : String) (amount : Int) : CommandRequest

HINCRBY key field increment

Equations

• LeanRedis.CommandRequest.hIncrBy key field amount = { name := "HINCRBY", args := LeanRedis.CommandRequest.utf8Args #[key, field, toString amount] }

def LeanRedis.CommandRequest.hIncrByFloat (key field amount : String) : CommandRequest

HINCRBYFLOAT key field increment

Equations

• LeanRedis.CommandRequest.hIncrByFloat key field amount = { name := "HINCRBYFLOAT", args := LeanRedis.CommandRequest.utf8Args #[key, field, amount] }

def LeanRedis.CommandRequest.hSetNx (key field value : String) : CommandRequest

HSETNX key field value

Equations

• LeanRedis.CommandRequest.hSetNx key field value = { name := "HSETNX", args := LeanRedis.CommandRequest.utf8Args #[key, field, value] }

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

HRANDFIELD key [count [WITHVALUES]]

Equations

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

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

HRANDFIELD key count

Equations

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

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

HRANDFIELD key count WITHVALUES

Equations

• LeanRedis.CommandRequest.hRandFieldsWithValues key count = { name := "HRANDFIELD", args := LeanRedis.CommandRequest.utf8Args #[key, toString count, "WITHVALUES"] }

def LeanRedis.CommandRequest.hScan (key : String) (cursor : UInt64) (options : HScanOptions := { }) : CommandRequest

HSCAN key cursor [MATCH pattern] [COUNT count]

Equations

• LeanRedis.CommandRequest.hScan key cursor options = { name := "HSCAN", args := LeanRedis.CommandRequest.utf8Args #[key, toString cursor] ++ LeanRedis.CommandRequest.hScanArgs options }

def LeanRedis.Command.hGet (key field : String) : Command (Option String)

Equations

• LeanRedis.Command.hGet key field = { request := LeanRedis.CommandRequest.hGet key field, decode := LeanRedis.expectOptionalString "HGET" }

def LeanRedis.Command.hSet (key : String) (entries : Array (String × String)) : Command Int

Equations

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

def LeanRedis.Command.hMGet (key : String) (fields : Array String) : Command (Array (Option String))

Equations

• LeanRedis.Command.hMGet key fields = { request := LeanRedis.CommandRequest.hMGet key fields, decode := LeanRedis.expectStringArray "HMGET" }

def LeanRedis.Command.hMSet (key : String) (entries : Array (String × String)) : Command Unit

Equations

• LeanRedis.Command.hMSet key entries = { request := LeanRedis.CommandRequest.hMSet key entries, decode := LeanRedis.expectOk }

def LeanRedis.Command.hGetAll (key : String) : Command (Array (String × String))

Equations

• LeanRedis.Command.hGetAll key = { request := LeanRedis.CommandRequest.hGetAll key, decode := LeanRedis.expectStringPairs "HGETALL" }

def LeanRedis.Command.hDel (key : String) (fields : Array String) : Command Int

Equations

• LeanRedis.Command.hDel key fields = { request := LeanRedis.CommandRequest.hDel key fields, decode := LeanRedis.expectInteger "HDEL" }

def LeanRedis.Command.hExists (key field : String) : Command Bool

Equations

• LeanRedis.Command.hExists key field = { request := LeanRedis.CommandRequest.hExists key field, decode := LeanRedis.expectBoolean "HEXISTS" }

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

Equations

• LeanRedis.Command.hLen key = { request := LeanRedis.CommandRequest.hLen key, decode := LeanRedis.expectInteger "HLEN" }

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

Equations

• LeanRedis.Command.hKeys key = { request := LeanRedis.CommandRequest.hKeys key, decode := LeanRedis.expectPlainStringArray "HKEYS" }

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

Equations

• LeanRedis.Command.hVals key = { request := LeanRedis.CommandRequest.hVals key, decode := LeanRedis.expectPlainStringArray "HVALS" }

def LeanRedis.Command.hStrLen (key field : String) : Command Int

Equations

• LeanRedis.Command.hStrLen key field = { request := LeanRedis.CommandRequest.hStrLen key field, decode := LeanRedis.expectInteger "HSTRLEN" }

def LeanRedis.Command.hIncrBy (key field : String) (amount : Int) : Command Int

Equations

• LeanRedis.Command.hIncrBy key field amount = { request := LeanRedis.CommandRequest.hIncrBy key field amount, decode := LeanRedis.expectInteger "HINCRBY" }

def LeanRedis.Command.hIncrByFloat (key field amount : String) : Command String

Equations

• LeanRedis.Command.hIncrByFloat key field amount = { request := LeanRedis.CommandRequest.hIncrByFloat key field amount, decode := LeanRedis.expectString "HINCRBYFLOAT" }

def LeanRedis.Command.hSetNx (key field value : String) : Command Bool

Equations

• LeanRedis.Command.hSetNx key field value = { request := LeanRedis.CommandRequest.hSetNx key field value, decode := LeanRedis.expectBoolean "HSETNX" }

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

Equations

• LeanRedis.Command.hRandField key = { request := LeanRedis.CommandRequest.hRandField key, decode := LeanRedis.expectOptionalString "HRANDFIELD" }

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

Equations

• LeanRedis.Command.hRandFields key count = { request := LeanRedis.CommandRequest.hRandFields key count, decode := LeanRedis.expectPlainStringArray "HRANDFIELD" }

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

Equations

• LeanRedis.Command.hRandFieldsWithValues key count = { request := LeanRedis.CommandRequest.hRandFieldsWithValues key count, decode := LeanRedis.expectStringPairs "HRANDFIELD" }

def LeanRedis.Command.hScan (key : String) (cursor : UInt64) (options : HScanOptions := { }) : Command HashScanResult

Equations

• LeanRedis.Command.hScan key cursor options = { request := LeanRedis.CommandRequest.hScan key cursor options, decode := LeanRedis.expectHScanResult }