def LeanRedis.Client.copy {τ : Type} [Transport.Transport τ] (client : Client τ) (source destination : String) (options : CopyOptions := { }) : Std.Internal.IO.Async.Async Bool

Copy a key to a new key.

Example:

let copied ← client.copy "src" "dst"

Equations

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

def LeanRedis.Client.del {τ : Type} [Transport.Transport τ] (client : Client τ) (keys : Array String) : Std.Internal.IO.Async.Async Int

Delete one or more keys.

Example:

let removed ← client.del #["key1", "key2"]

Equations

• client.del keys = do let reply ← client.execute (LeanRedis.Command.del keys).request liftM ((LeanRedis.Command.del keys).decode reply)

def LeanRedis.Client.dump {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async String

Dump a serialised version of the value stored at a key.

Example:

let serialized ← client.dump "key"

Equations

• client.dump key = do let reply ← client.execute (LeanRedis.Command.dump key).request liftM ((LeanRedis.Command.dump key).decode reply)

def LeanRedis.Client.exists {τ : Type} [Transport.Transport τ] (client : Client τ) (keys : Array String) : Std.Internal.IO.Async.Async Int

Determine whether one or more keys exist.

Example:

let count ← client.exists #["key1", "key2"]

Equations

• client.exists keys = do let reply ← client.execute (LeanRedis.Command.exists keys).request liftM ((LeanRedis.Command.exists keys).decode reply)

def LeanRedis.Client.expire {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (seconds : UInt64) (option : Option ExpireOption := none) : Std.Internal.IO.Async.Async Bool

Set a key's time to live in seconds.

Example:

let set ← client.expire "key" 60

Equations

• client.expire key seconds option = do let reply ← client.execute (LeanRedis.Command.expire key seconds option).request liftM ((LeanRedis.Command.expire key seconds option).decode reply)

def LeanRedis.Client.expireAt {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : Std.Internal.IO.Async.Async Bool

Set a key's time to live as a Unix timestamp in seconds.

Example:

let set ← client.expireAt "key" timestamp

Equations

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

def LeanRedis.Client.expireTime {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the expiration time of a key as a Unix timestamp in seconds.

Example:

let ts ← client.expireTime "key"

Equations

• client.expireTime key = do let reply ← client.execute (LeanRedis.Command.expireTime key).request liftM ((LeanRedis.Command.expireTime key).decode reply)

def LeanRedis.Client.keys {τ : Type} [Transport.Transport τ] (client : Client τ) (pattern : String) : Std.Internal.IO.Async.Async (Array String)

Find all keys matching the given pattern.

Example:

let keys ← client.keys "user:*"

Equations

• client.keys pattern = do let reply ← client.execute (LeanRedis.Command.keys pattern).request liftM ((LeanRedis.Command.keys pattern).decode reply)

def LeanRedis.Client.move {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (destinationDb : UInt32) : Std.Internal.IO.Async.Async Bool

Move a key to another database.

Example:

let moved ← client.move "key" 1

Equations

• client.move key destinationDb = do let reply ← client.execute (LeanRedis.Command.move key destinationDb).request liftM ((LeanRedis.Command.move key destinationDb).decode reply)

def LeanRedis.Client.objectEncoding {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async String

Get the internal encoding of a key's value.

Example:

let encoding ← client.objectEncoding "key"

Equations

• client.objectEncoding key = do let reply ← client.execute (LeanRedis.Command.objectEncoding key).request liftM ((LeanRedis.Command.objectEncoding key).decode reply)

def LeanRedis.Client.objectFreq {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the logarithmic access frequency counter of a key's value.

Example:

let freq ← client.objectFreq "key"

Equations

• client.objectFreq key = do let reply ← client.execute (LeanRedis.Command.objectFreq key).request liftM ((LeanRedis.Command.objectFreq key).decode reply)

def LeanRedis.Client.objectIdleTime {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the idle time of a key in seconds.

Example:

let idle ← client.objectIdleTime "key"

Equations

• client.objectIdleTime key = do let reply ← client.execute (LeanRedis.Command.objectIdleTime key).request liftM ((LeanRedis.Command.objectIdleTime key).decode reply)

def LeanRedis.Client.objectRefCount {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the reference count of a key's value.

Example:

let refcount ← client.objectRefCount "key"

Equations

• client.objectRefCount key = do let reply ← client.execute (LeanRedis.Command.objectRefCount key).request liftM ((LeanRedis.Command.objectRefCount key).decode reply)

def LeanRedis.Client.persist {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Bool

Remove the expiration from a key.

Example:

let removed ← client.persist "key"

Equations

• client.persist key = do let reply ← client.execute (LeanRedis.Command.persist key).request liftM ((LeanRedis.Command.persist key).decode reply)

def LeanRedis.Client.pexpire {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (milliseconds : UInt64) (option : Option ExpireOption := none) : Std.Internal.IO.Async.Async Bool

Set a key's time to live in milliseconds.

Example:

let set ← client.pexpire "key" 5000

Equations

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

def LeanRedis.Client.pexpireAt {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (timestamp : Std.Time.Timestamp) (option : Option ExpireOption := none) : Std.Internal.IO.Async.Async Bool

Set a key's time to live as a Unix timestamp in milliseconds.

Example:

let set ← client.pexpireAt "key" timestamp

Equations

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

def LeanRedis.Client.pttl {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the time to live for a key in milliseconds.

Example:

let ttl ← client.pttl "key"

Equations

• client.pttl key = do let reply ← client.execute (LeanRedis.Command.pttl key).request liftM ((LeanRedis.Command.pttl key).decode reply)

def LeanRedis.Client.randomKey {τ : Type} [Transport.Transport τ] (client : Client τ) : Std.Internal.IO.Async.Async (Option String)

Return a random key from the keyspace.

Example:

let key ← client.randomKey

Equations

• client.randomKey = do let reply ← client.execute LeanRedis.Command.randomKey.request liftM (LeanRedis.Command.randomKey.decode reply)

def LeanRedis.Client.rename {τ : Type} [Transport.Transport τ] (client : Client τ) (key newKey : String) : Std.Internal.IO.Async.Async Unit

Rename a key.

Example:

let _ ← client.rename "old" "new"

Equations

• client.rename key newKey = do let reply ← client.execute (LeanRedis.Command.rename key newKey).request liftM ((LeanRedis.Command.rename key newKey).decode reply)

def LeanRedis.Client.renameNx {τ : Type} [Transport.Transport τ] (client : Client τ) (key newKey : String) : Std.Internal.IO.Async.Async Bool

Rename a key only when the target key does not exist.

Example:

let renamed ← client.renameNx "old" "new"

Equations

• client.renameNx key newKey = do let reply ← client.execute (LeanRedis.Command.renameNx key newKey).request liftM ((LeanRedis.Command.renameNx key newKey).decode reply)

def LeanRedis.Client.restore {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (ttl : UInt64) (serializedValue : String) (options : RestoreOptions := { }) : Std.Internal.IO.Async.Async Unit

Restore a serialised value previously obtained with DUMP.

Example:

let _ ← client.restore "key" 0 serialized

Equations

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

def LeanRedis.Client.scan {τ : Type} [Transport.Transport τ] (client : Client τ) (cursor : UInt64) (options : ScanOptions := { }) : Std.Internal.IO.Async.Async ScanResult

Incrementally iterate the keyspace.

Example:

let page ← client.scan 0

Equations

• client.scan cursor options = do let reply ← client.execute (LeanRedis.Command.scan cursor options).request liftM ((LeanRedis.Command.scan cursor options).decode reply)

def LeanRedis.Client.sort {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (options : SortOptions := { }) : Std.Internal.IO.Async.Async (Array String)

Sort the elements in a list, set, or sorted set.

NOTE: When using the store? option, Redis returns the number of stored elements rather than the sorted array. This method expects an array reply; use execute directly when STORE is specified.

Example:

let elements ← client.sort "mylist"

Equations

• client.sort key options = do let reply ← client.execute (LeanRedis.Command.sort key options).request liftM ((LeanRedis.Command.sort key options).decode reply)

def LeanRedis.Client.sortRo {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (options : SortRoOptions := { }) : Std.Internal.IO.Async.Async (Array String)

Sort the elements in a list, set, or sorted set (read‑only variant).

Example:

let elements ← client.sortRo "mylist"

Equations

• client.sortRo key options = do let reply ← client.execute (LeanRedis.Command.sortRo key options).request liftM ((LeanRedis.Command.sortRo key options).decode reply)

def LeanRedis.Client.touch {τ : Type} [Transport.Transport τ] (client : Client τ) (keys : Array String) : Std.Internal.IO.Async.Async Int

Touch one or more keys, updating their access time.

Example:

let touched ← client.touch #["key1", "key2"]

Equations

• client.touch keys = do let reply ← client.execute (LeanRedis.Command.touch keys).request liftM ((LeanRedis.Command.touch keys).decode reply)

def LeanRedis.Client.ttl {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async Int

Get the time to live for a key in seconds.

Example:

let ttl ← client.ttl "key"

Equations

• client.ttl key = do let reply ← client.execute (LeanRedis.Command.TTL key).request liftM ((LeanRedis.Command.TTL key).decode reply)

def LeanRedis.Client.type {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) : Std.Internal.IO.Async.Async String

Determine the type of the value stored at a key.

Example:

let type ← client.type "key"

Equations

• client.type key = do let reply ← client.execute (LeanRedis.Command.type key).request liftM ((LeanRedis.Command.type key).decode reply)

def LeanRedis.Client.unlink {τ : Type} [Transport.Transport τ] (client : Client τ) (keys : Array String) : Std.Internal.IO.Async.Async Int

Delete one or more keys asynchronously (non‑blocking).

Example:

let unlinked ← client.unlink #["key1", "key2"]

Equations

• client.unlink keys = do let reply ← client.execute (LeanRedis.Command.unlink keys).request liftM ((LeanRedis.Command.unlink keys).decode reply)