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

Push values to the left side of a list.

Example:

let len ← client.lPush "jobs" #["a", "b"]

Equations

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

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

Push values to the right side of a list.

Example:

let len ← client.rPush "jobs" #["a", "b"]

Equations

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

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

Push a value to the left only if the list already exists.

Example:

let len ← client.lPushX "jobs" "a"

Equations

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

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

Push a value to the right only if the list already exists.

Example:

let len ← client.rPushX "jobs" "a"

Equations

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

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

Pop one value from the left side of a list.

Example:

let value ← client.lPop "jobs"

Equations

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

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

Pop one value from the right side of a list.

Example:

let value ← client.rPop "jobs"

Equations

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

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

Return the current length of a list.

Example:

let len ← client.lLen "jobs"

Equations

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

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

Return the value at a list index.

Example:

let value ← client.lIndex "jobs" 0

Equations

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

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

Return a range of list elements.

Example:

let values ← client.lRange "jobs" 0 (-1)

Equations

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

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

Replace the value at a list index.

Example:

let _ ← client.lSet "jobs" 0 "next"

Equations

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

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

Trim a list to the given inclusive range.

Example:

let _ ← client.lTrim "jobs" 0 9

Equations

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

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

Remove matching elements from a list.

Example:

let removed ← client.lRem "jobs" 0 "done"

Equations

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

def LeanRedis.Client.lInsert {τ : Type} [Transport.Transport τ] (client : Client τ) (key : String) (position : LInsertPosition) (pivot value : String) : Std.Internal.IO.Async.Async Int

Insert a value before or after a pivot element.

Example:

let index ← client.lInsert "jobs" .after "a" "b"

Equations

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

def LeanRedis.Client.lMove {τ : Type} [Transport.Transport τ] (client : Client τ) (source destination : String) (fromWhere toWhere : LMoveWhere) : Std.Internal.IO.Async.Async (Option String)

Move one element between lists.

Example:

let value ← client.lMove "jobs" "done" .left .right

Equations

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

def LeanRedis.Client.lPos {τ : Type} [Transport.Transport τ] (client : Client τ) (key element : String) (options : LPosOptions := { }) : Std.Internal.IO.Async.Async (Option Int)

Return a single matching position from LPOS.

Example:

let pos ← client.lPos "jobs" "a"

Equations

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

def LeanRedis.Client.lPosMany {τ : Type} [Transport.Transport τ] (client : Client τ) (key element : String) (options : LPosOptions) : Std.Internal.IO.Async.Async (Array Int)

Return multiple matching positions from LPOS.

Example:

let positions ← client.lPosMany "jobs" "a" { count? := some 3 }

Equations

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