def LeanRedis.Pipeline.lPush {α : List Type} (pipeline : Pipeline α) (key : String) (values : Array String) : Pipeline (α ++ [Int])

Equations

• pipeline.lPush key values = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lPush key values))

def LeanRedis.Pipeline.rPush {α : List Type} (pipeline : Pipeline α) (key : String) (values : Array String) : Pipeline (α ++ [Int])

Equations

• pipeline.rPush key values = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.rPush key values))

def LeanRedis.Pipeline.lPushX {α : List Type} (pipeline : Pipeline α) (key value : String) : Pipeline (α ++ [Int])

Equations

• pipeline.lPushX key value = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lPushX key value))

def LeanRedis.Pipeline.rPushX {α : List Type} (pipeline : Pipeline α) (key value : String) : Pipeline (α ++ [Int])

Equations

• pipeline.rPushX key value = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.rPushX key value))

def LeanRedis.Pipeline.lPop {α : List Type} (pipeline : Pipeline α) (key : String) : Pipeline (α ++ [Option String])

Equations

• pipeline.lPop key = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lPop key))

def LeanRedis.Pipeline.rPop {α : List Type} (pipeline : Pipeline α) (key : String) : Pipeline (α ++ [Option String])

Equations

• pipeline.rPop key = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.rPop key))

def LeanRedis.Pipeline.lLen {α : List Type} (pipeline : Pipeline α) (key : String) : Pipeline (α ++ [Int])

Equations

• pipeline.lLen key = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lLen key))

def LeanRedis.Pipeline.lIndex {α : List Type} (pipeline : Pipeline α) (key : String) (index : Int) : Pipeline (α ++ [Option String])

Equations

• pipeline.lIndex key index = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lIndex key index))

def LeanRedis.Pipeline.lRange {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) : Pipeline (α ++ [Array String])

Equations

• pipeline.lRange key start stop = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lRange key start stop))

def LeanRedis.Pipeline.lSet {α : List Type} (pipeline : Pipeline α) (key : String) (index : Int) (value : String) : Pipeline (α ++ [Unit])

Equations

• pipeline.lSet key index value = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lSet key index value))

def LeanRedis.Pipeline.lTrim {α : List Type} (pipeline : Pipeline α) (key : String) (start stop : Int) : Pipeline (α ++ [Unit])

Equations

• pipeline.lTrim key start stop = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lTrim key start stop))

def LeanRedis.Pipeline.lRem {α : List Type} (pipeline : Pipeline α) (key : String) (count : Int) (value : String) : Pipeline (α ++ [Int])

Equations

• pipeline.lRem key count value = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lRem key count value))

def LeanRedis.Pipeline.lInsert {α : List Type} (pipeline : Pipeline α) (key : String) (position : LInsertPosition) (pivot value : String) : Pipeline (α ++ [Int])

Equations

• pipeline.lInsert key position pivot value = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lInsert key position pivot value))

def LeanRedis.Pipeline.lMove {α : List Type} (pipeline : Pipeline α) (source destination : String) (fromWhere toWhere : LMoveWhere) : Pipeline (α ++ [Option String])

Equations

• pipeline.lMove source destination fromWhere toWhere = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lMove source destination fromWhere toWhere))

def LeanRedis.Pipeline.lPos {α : List Type} (pipeline : Pipeline α) (key element : String) (options : LPosOptions := { }) : Pipeline (α ++ [Option Int])

Equations

• pipeline.lPos key element options = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lPos key element options))

def LeanRedis.Pipeline.lPosMany {α : List Type} (pipeline : Pipeline α) (key element : String) (options : LPosOptions) : Pipeline (α ++ [Array Int])

Equations

• pipeline.lPosMany key element options = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.lPosMany key element options))