Generic commands

This module contains implementations of commands that don't fit into a more specific category. For example, the PING command is implemented here since it doesn't belong to a specific data type category like strings or hashes.

• COPY
• DEL
• DUMP
• EXISTS
• EXPIRE
• EXPIREAT
• EXPIRETIME
• KEYS
• MIGRATE
• MOVE
• OBJECT ENCODING
• OBJECT FREQ
• OBJECT IDLETIME
• OBJECT REFCOUNT
• PERSIST
• PEXPIRE
• PEXPIREAT
• PTTL
• RANDOMKEY
• RENAME
• RENAMENX
• RESTORE
• SCAN
• SORT
• SORT_RO
• TOUCH
• TTL
• TYPE
• UNLINK

structure LeanRedis.CopyOptions : Type

• db? : Option UInt32
• replace : Bool

def LeanRedis.instBEqCopyOptions.beq : CopyOptions → CopyOptions → Bool

Equations

• LeanRedis.instBEqCopyOptions.beq { db? := a, replace := a_1 } { db? := b, replace := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqCopyOptions.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqCopyOptions : BEq CopyOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedCopyOptions : Inhabited CopyOptions

Equations

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

def LeanRedis.instInhabitedCopyOptions.default : CopyOptions

Equations

• LeanRedis.instInhabitedCopyOptions.default = { db? := default, replace := default }

def LeanRedis.instReprCopyOptions.repr : CopyOptions → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprCopyOptions : Repr CopyOptions

Equations

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

def LeanRedis.CommandRequest.copy (source destination : String) (options : CopyOptions := { }) : CommandRequest

COPY source destination [DB db] [REPLACE]

Equations

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

def LeanRedis.Command.copy (source destination : String) (options : CopyOptions := { }) : Command Bool

Equations

• LeanRedis.Command.copy source destination options = { request := LeanRedis.CommandRequest.copy source destination options, decode := LeanRedis.expectBoolean "COPY" }

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

DEL key [key ...]

Equations

• LeanRedis.CommandRequest.del keys = { name := "DEL", args := LeanRedis.CommandRequest.utf8Args keys }

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

Equations

• LeanRedis.Command.del keys = { request := LeanRedis.CommandRequest.del keys, decode := LeanRedis.expectInteger "DEL" }

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

DUMP key

Equations

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

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

TTL key

Equations

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

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

EXISTS key [key ...]

Equations

• LeanRedis.CommandRequest.exists keys = { name := "EXISTS", args := LeanRedis.CommandRequest.utf8Args keys }

inductive LeanRedis.ExpireOption : Type

• NX : ExpireOption
• XX : ExpireOption
• GT : ExpireOption
• LT : ExpireOption

def LeanRedis.instBEqExpireOption.beq : ExpireOption → ExpireOption → Bool

Equations

• LeanRedis.instBEqExpireOption.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance LeanRedis.instBEqExpireOption : BEq ExpireOption

Equations

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

def LeanRedis.instInhabitedExpireOption.default : ExpireOption

Equations

• LeanRedis.instInhabitedExpireOption.default = LeanRedis.ExpireOption.NX

@[implicit_reducible]

instance LeanRedis.instInhabitedExpireOption : Inhabited ExpireOption

Equations

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

def LeanRedis.instReprExpireOption.repr : ExpireOption → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprExpireOption : Repr ExpireOption

Equations

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

@[implicit_reducible]

instance LeanRedis.instToStringExpireOption : ToString ExpireOption

Equations

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

def LeanRedis.CommandRequest.expire (key : String) (seconds : UInt64) (option : Option ExpireOption := none) : CommandRequest

EXPIRE key seconds [NX | XX | GT | LT]

Equations

• LeanRedis.CommandRequest.expire key seconds (some opt) = { name := "EXPIRE", args := LeanRedis.CommandRequest.utf8Args (#[key, toString seconds] ++ #[toString opt]) }
• LeanRedis.CommandRequest.expire key seconds = { name := "EXPIRE", args := LeanRedis.CommandRequest.utf8Args (#[key, toString seconds] ++ #[]) }

def LeanRedis.CommandRequest.expireAt (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : CommandRequest

EXPIREAT key unix-time-seconds [NX | XX | GT | LT]

Equations

• LeanRedis.CommandRequest.expireAt key timestamp (some opt) = { name := "EXPIREAT", args := LeanRedis.CommandRequest.utf8Args (#[key, toString timestamp] ++ #[toString opt]) }
• LeanRedis.CommandRequest.expireAt key timestamp = { name := "EXPIREAT", args := LeanRedis.CommandRequest.utf8Args (#[key, toString timestamp] ++ #[]) }

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

EXPIRETIME key

Equations

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

def LeanRedis.CommandRequest.keys (pattern : String) : CommandRequest

KEYS pattern

Equations

• LeanRedis.CommandRequest.keys pattern = { name := "KEYS", args := LeanRedis.CommandRequest.utf8Args #[pattern] }

structure LeanRedis.MigrateOptions : Type

• copy : Bool
• replace : Bool
• auth : Option AuthConfig

def LeanRedis.CommandRequest.migrate (host : String) (port : UInt16) (keys : Array String) (destinationDb : UInt32 := 0) (timeout : UInt64 := 5000) (options : MigrateOptions := { }) : CommandRequest

MIGRATE host port key|"" destination-db timeout [COPY] [REPLACE] [AUTH password] [AUTH2 username password] [KEYS key [key ...]]

Equations

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

def LeanRedis.CommandRequest.move (key : String) (destinationDb : UInt32) : CommandRequest

MOVE key db

Equations

• LeanRedis.CommandRequest.move key destinationDb = { name := "MOVE", args := LeanRedis.CommandRequest.utf8Args #[key, toString destinationDb] }

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

OBJECT ENCODING key

Equations

• LeanRedis.CommandRequest.objectEncoding key = { name := "OBJECT ENCODING", args := LeanRedis.CommandRequest.utf8Args #[key] }

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

OBJECT FREQ key

Equations

• LeanRedis.CommandRequest.objectFreq key = { name := "OBJECT FREQ", args := LeanRedis.CommandRequest.utf8Args #[key] }

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

OBJECT IDLETIME key

Equations

• LeanRedis.CommandRequest.objectIdleTime key = { name := "OBJECT IDLETIME", args := LeanRedis.CommandRequest.utf8Args #[key] }

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

OBJECT REFCOUNT key

Equations

• LeanRedis.CommandRequest.objectRefCount key = { name := "OBJECT REFCOUNT", args := LeanRedis.CommandRequest.utf8Args #[key] }

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

PERSIST key

Equations

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

def LeanRedis.CommandRequest.pexpire (key : String) (milliseconds : UInt64) (option : Option ExpireOption := none) : CommandRequest

PEXPIRE key milliseconds [NX | XX | GT | LT]

Equations

• LeanRedis.CommandRequest.pexpire key milliseconds (some opt) = { name := "PEXPIRE", args := LeanRedis.CommandRequest.utf8Args (#[key, toString milliseconds] ++ #[toString opt]) }
• LeanRedis.CommandRequest.pexpire key milliseconds = { name := "PEXPIRE", args := LeanRedis.CommandRequest.utf8Args (#[key, toString milliseconds] ++ #[]) }

def LeanRedis.CommandRequest.pexpireAt (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : CommandRequest

PEXPIREAT key unix-time-milliseconds [NX | XX | GT | LT]

Equations

• LeanRedis.CommandRequest.pexpireAt key timestamp (some opt) = { name := "PEXPIREAT", args := LeanRedis.CommandRequest.utf8Args (#[key, toString timestamp] ++ #[toString opt]) }
• LeanRedis.CommandRequest.pexpireAt key timestamp = { name := "PEXPIREAT", args := LeanRedis.CommandRequest.utf8Args (#[key, toString timestamp] ++ #[]) }

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

PTTL key

Equations

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

def LeanRedis.CommandRequest.randomKey : CommandRequest

RANDOMKEY

Equations

• LeanRedis.CommandRequest.randomKey = { name := "RANDOMKEY" }

def LeanRedis.CommandRequest.rename (key newKey : String) : CommandRequest

RENAME key newkey

Equations

• LeanRedis.CommandRequest.rename key newKey = { name := "RENAME", args := LeanRedis.CommandRequest.utf8Args #[key, newKey] }

def LeanRedis.CommandRequest.renameNx (key newKey : String) : CommandRequest

RENAMENX key newkey

Equations

• LeanRedis.CommandRequest.renameNx key newKey = { name := "RENAMENX", args := LeanRedis.CommandRequest.utf8Args #[key, newKey] }

structure LeanRedis.RestoreOptions : Type

• replace : Bool
• absTTL : Bool
• idleTime? : Option UInt64
• frequency? : Option UInt64

def LeanRedis.CommandRequest.restore (key : String) (ttl : UInt64) (serializedValue : String) (options : RestoreOptions := { }) : CommandRequest

RESTORE key ttl serialized-value [REPLACE] [ABSTTL] [IDLETIME time] [FREQ freq]

Equations

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

structure LeanRedis.ScanOptions : Type

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

def LeanRedis.CommandRequest.scan (cursor : UInt64) (options : ScanOptions := { }) : CommandRequest

SCAN cursor [MATCH pattern] [COUNT count] [TYPE type]

Equations

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

structure LeanRedis.SortOptions : Type

• by? : Option String
• limit? : Option (UInt64 × UInt64)
• getPatterns : Array String
• asc? : Option Bool
• alpha : Bool
• store? : Option String

def LeanRedis.CommandRequest.sort (key : String) (options : SortOptions := { }) : CommandRequest

SORT key [BY pattern] [LIMIT offset count] [GET pattern [GET pattern ...]] [ASC | DESC] [ALPHA] [STORE destination]

Equations

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

structure LeanRedis.SortRoOptions : Type

• by? : Option String
• limit? : Option (UInt64 × UInt64)
• getPatterns : Array String
• asc? : Option Bool
• alpha : Bool

def LeanRedis.CommandRequest.sortRo (key : String) (options : SortRoOptions := { }) : CommandRequest

SORT_RO key [BY pattern] [LIMIT offset count] [GET pattern [GET pattern ...]] [ASC | DESC] [ALPHA]

Equations

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

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

TOUCH key [key ...]

Equations

• LeanRedis.CommandRequest.touch keys = { name := "TOUCH", args := LeanRedis.CommandRequest.utf8Args keys }

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

TTL key

Equations

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

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

TYPE key

Equations

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

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

UNLINK key [key ...]

Equations

• LeanRedis.CommandRequest.unlink keys = { name := "UNLINK", args := LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.Command.dump (key : String) : Command String

Equations

• LeanRedis.Command.dump key = { request := LeanRedis.CommandRequest.dump key, decode := LeanRedis.expectString "DUMP" }

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

Equations

• LeanRedis.Command.exists keys = { request := LeanRedis.CommandRequest.exists keys, decode := LeanRedis.expectInteger "EXISTS" }

def LeanRedis.Command.expire (key : String) (seconds : UInt64) (option : Option ExpireOption := none) : Command Bool

Equations

• LeanRedis.Command.expire key seconds option = { request := LeanRedis.CommandRequest.expire key seconds option, decode := LeanRedis.expectBoolean "EXPIRE" }

def LeanRedis.Command.expireAt (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : Command Bool

Equations

• LeanRedis.Command.expireAt key timestamp option = { request := LeanRedis.CommandRequest.expireAt key timestamp option, decode := LeanRedis.expectBoolean "EXPIREAT" }

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

Equations

• LeanRedis.Command.expireTime key = { request := LeanRedis.CommandRequest.expireTime key, decode := LeanRedis.expectInteger "EXPIRETIME" }

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

Equations

• LeanRedis.Command.keys pattern = { request := LeanRedis.CommandRequest.keys pattern, decode := LeanRedis.expectPlainStringArray "KEYS" }

def LeanRedis.Command.move (key : String) (destinationDb : UInt32) : Command Bool

Equations

• LeanRedis.Command.move key destinationDb = { request := LeanRedis.CommandRequest.move key destinationDb, decode := LeanRedis.expectBoolean "MOVE" }

def LeanRedis.Command.objectEncoding (key : String) : Command String

Equations

• LeanRedis.Command.objectEncoding key = { request := LeanRedis.CommandRequest.objectEncoding key, decode := LeanRedis.expectString "OBJECT ENCODING" }

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

Equations

• LeanRedis.Command.objectFreq key = { request := LeanRedis.CommandRequest.objectFreq key, decode := LeanRedis.expectInteger "OBJECT FREQ" }

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

Equations

• LeanRedis.Command.objectIdleTime key = { request := LeanRedis.CommandRequest.objectIdleTime key, decode := LeanRedis.expectInteger "OBJECT IDLETIME" }

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

Equations

• LeanRedis.Command.objectRefCount key = { request := LeanRedis.CommandRequest.objectRefCount key, decode := LeanRedis.expectInteger "OBJECT REFCOUNT" }

def LeanRedis.Command.persist (key : String) : Command Bool

Equations

• LeanRedis.Command.persist key = { request := LeanRedis.CommandRequest.persist key, decode := LeanRedis.expectBoolean "PERSIST" }

def LeanRedis.Command.pexpire (key : String) (milliseconds : UInt64) (option : Option ExpireOption := none) : Command Bool

Equations

• LeanRedis.Command.pexpire key milliseconds option = { request := LeanRedis.CommandRequest.pexpire key milliseconds option, decode := LeanRedis.expectBoolean "PEXPIRE" }

def LeanRedis.Command.pexpireAt (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : Command Bool

Equations

• LeanRedis.Command.pexpireAt key timestamp option = { request := LeanRedis.CommandRequest.pexpireAt key timestamp option, decode := LeanRedis.expectBoolean "PEXPIREAT" }

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

Equations

• LeanRedis.Command.pttl key = { request := LeanRedis.CommandRequest.pttl key, decode := LeanRedis.expectInteger "PTTL" }

def LeanRedis.Command.randomKey : Command (Option String)

Equations

• LeanRedis.Command.randomKey = { request := LeanRedis.CommandRequest.randomKey, decode := LeanRedis.expectOptionalString "RANDOMKEY" }

def LeanRedis.Command.rename (key newKey : String) : Command Unit

Equations

• LeanRedis.Command.rename key newKey = { request := LeanRedis.CommandRequest.rename key newKey, decode := LeanRedis.expectOk }

def LeanRedis.Command.renameNx (key newKey : String) : Command Bool

Equations

• LeanRedis.Command.renameNx key newKey = { request := LeanRedis.CommandRequest.renameNx key newKey, decode := LeanRedis.expectBoolean "RENAMENX" }

def LeanRedis.Command.restore (key : String) (ttl : UInt64) (serializedValue : String) (options : RestoreOptions := { }) : Command Unit

Equations

• LeanRedis.Command.restore key ttl serializedValue options = { request := LeanRedis.CommandRequest.restore key ttl serializedValue options, decode := LeanRedis.expectOk }

def LeanRedis.Command.scan (cursor : UInt64) (options : ScanOptions := { }) : Command ScanResult

Equations

• LeanRedis.Command.scan cursor options = { request := LeanRedis.CommandRequest.scan cursor options, decode := LeanRedis.expectScanResult }

def LeanRedis.Command.sort (key : String) (options : SortOptions := { }) : Command (Array String)

Equations

• LeanRedis.Command.sort key options = { request := LeanRedis.CommandRequest.sort key options, decode := LeanRedis.expectPlainStringArray "SORT" }

def LeanRedis.Command.sortRo (key : String) (options : SortRoOptions := { }) : Command (Array String)

Equations

• LeanRedis.Command.sortRo key options = { request := LeanRedis.CommandRequest.sortRo key options, decode := LeanRedis.expectPlainStringArray "SORT_RO" }

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

Equations

• LeanRedis.Command.touch keys = { request := LeanRedis.CommandRequest.touch keys, decode := LeanRedis.expectInteger "TOUCH" }

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

Equations

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

def LeanRedis.Command.type (key : String) : Command String

Equations

• LeanRedis.Command.type key = { request := LeanRedis.CommandRequest.type key, decode := LeanRedis.expectString "TYPE" }

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

Equations

• LeanRedis.Command.unlink keys = { request := LeanRedis.CommandRequest.unlink keys, decode := LeanRedis.expectInteger "UNLINK" }