inductive LeanRedis.LInsertPosition : Type

• before : LInsertPosition
• after : LInsertPosition

@[implicit_reducible]

instance LeanRedis.instBEqLInsertPosition : BEq LInsertPosition

Equations

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

def LeanRedis.instBEqLInsertPosition.beq : LInsertPosition → LInsertPosition → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedLInsertPosition : Inhabited LInsertPosition

Equations

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

def LeanRedis.instInhabitedLInsertPosition.default : LInsertPosition

Equations

• LeanRedis.instInhabitedLInsertPosition.default = LeanRedis.LInsertPosition.before

@[implicit_reducible]

instance LeanRedis.instReprLInsertPosition : Repr LInsertPosition

Equations

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

def LeanRedis.instReprLInsertPosition.repr : LInsertPosition → Nat → Std.Format

Equations

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

inductive LeanRedis.LMoveWhere : Type

• left : LMoveWhere
• right : LMoveWhere

def LeanRedis.instBEqLMoveWhere.beq : LMoveWhere → LMoveWhere → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.instBEqLMoveWhere : BEq LMoveWhere

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedLMoveWhere : Inhabited LMoveWhere

Equations

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

def LeanRedis.instInhabitedLMoveWhere.default : LMoveWhere

Equations

• LeanRedis.instInhabitedLMoveWhere.default = LeanRedis.LMoveWhere.left

def LeanRedis.instReprLMoveWhere.repr : LMoveWhere → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.instReprLMoveWhere.repr LeanRedis.LMoveWhere.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LeanRedis.LMoveWhere.left")).group prec✝

@[implicit_reducible]

instance LeanRedis.instReprLMoveWhere : Repr LMoveWhere

Equations

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

structure LeanRedis.LPosOptions : Type

• rank? : Option Int
• count? : Option UInt64
• maxLen? : Option UInt64

def LeanRedis.instBEqLPosOptions.beq : LPosOptions → LPosOptions → Bool

Equations

• LeanRedis.instBEqLPosOptions.beq { rank? := a, count? := a_1, maxLen? := a_2 } { rank? := b, count? := b_1, maxLen? := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• LeanRedis.instBEqLPosOptions.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqLPosOptions : BEq LPosOptions

Equations

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

def LeanRedis.instInhabitedLPosOptions.default : LPosOptions

Equations

• LeanRedis.instInhabitedLPosOptions.default = { rank? := default, count? := default, maxLen? := default }

@[implicit_reducible]

instance LeanRedis.instInhabitedLPosOptions : Inhabited LPosOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprLPosOptions : Repr LPosOptions

Equations

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

def LeanRedis.instReprLPosOptions.repr : LPosOptions → Nat → Std.Format

Equations

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

def LeanRedis.CommandRequest.lInsertPositionArg (position : LInsertPosition) : String

Equations

• LeanRedis.CommandRequest.lInsertPositionArg LeanRedis.LInsertPosition.before = "BEFORE"
• LeanRedis.CommandRequest.lInsertPositionArg LeanRedis.LInsertPosition.after = "AFTER"

def LeanRedis.CommandRequest.lMoveWhereArg (where_ : LMoveWhere) : String

Equations

• LeanRedis.CommandRequest.lMoveWhereArg LeanRedis.LMoveWhere.left = "LEFT"
• LeanRedis.CommandRequest.lMoveWhereArg LeanRedis.LMoveWhere.right = "RIGHT"

def LeanRedis.CommandRequest.lPosArgs (options : LPosOptions) : Array ByteArray

Equations

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

def LeanRedis.CommandRequest.lPush (key : String) (values : Array String) : CommandRequest

LPUSH key element [element ...]

Equations

• LeanRedis.CommandRequest.lPush key values = { name := "LPUSH", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args values }

def LeanRedis.CommandRequest.rPush (key : String) (values : Array String) : CommandRequest

RPUSH key element [element ...]

Equations

• LeanRedis.CommandRequest.rPush key values = { name := "RPUSH", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.utf8Args values }

def LeanRedis.CommandRequest.lPushX (key value : String) : CommandRequest

LPUSHX key element

Equations

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

def LeanRedis.CommandRequest.rPushX (key value : String) : CommandRequest

RPUSHX key element

Equations

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

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

LPOP key [count]

Equations

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

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

RPOP key [count]

Equations

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

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

LLEN key

Equations

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

def LeanRedis.CommandRequest.lIndex (key : String) (index : Int) : CommandRequest

LINDEX key index

Equations

• LeanRedis.CommandRequest.lIndex key index = { name := "LINDEX", args := LeanRedis.CommandRequest.utf8Args #[key, toString index] }

def LeanRedis.CommandRequest.lRange (key : String) (start stop : Int) : CommandRequest

LRANGE key start stop

Equations

• LeanRedis.CommandRequest.lRange key start stop = { name := "LRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop] }

def LeanRedis.CommandRequest.lSet (key : String) (index : Int) (value : String) : CommandRequest

LSET key index value

Equations

• LeanRedis.CommandRequest.lSet key index value = { name := "LSET", args := LeanRedis.CommandRequest.utf8Args #[key, toString index, value] }

def LeanRedis.CommandRequest.lTrim (key : String) (start stop : Int) : CommandRequest

LTRIM key start stop

Equations

• LeanRedis.CommandRequest.lTrim key start stop = { name := "LTRIM", args := LeanRedis.CommandRequest.utf8Args #[key, toString start, toString stop] }

def LeanRedis.CommandRequest.lRem (key : String) (count : Int) (value : String) : CommandRequest

LREM key count value

Equations

• LeanRedis.CommandRequest.lRem key count value = { name := "LREM", args := LeanRedis.CommandRequest.utf8Args #[key, toString count, value] }

def LeanRedis.CommandRequest.lInsert (key : String) (position : LInsertPosition) (pivot value : String) : CommandRequest

LINSERT key BEFORE|AFTER pivot value

Equations

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

def LeanRedis.CommandRequest.lMove (source destination : String) (fromWhere toWhere : LMoveWhere) : CommandRequest

LMOVE source destination LEFT|RIGHT LEFT|RIGHT

Equations

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

def LeanRedis.CommandRequest.lPos (key element : String) (options : LPosOptions := { }) : CommandRequest

LPOS key element [RANK rank] [COUNT count] [MAXLEN maxlen]

Equations

• LeanRedis.CommandRequest.lPos key element options = { name := "LPOS", args := LeanRedis.CommandRequest.utf8Args #[key, element] ++ LeanRedis.CommandRequest.lPosArgs options }

def LeanRedis.Command.lPush (key : String) (values : Array String) : Command Int

Equations

• LeanRedis.Command.lPush key values = { request := LeanRedis.CommandRequest.lPush key values, decode := LeanRedis.expectInteger "LPUSH" }

def LeanRedis.Command.rPush (key : String) (values : Array String) : Command Int

Equations

• LeanRedis.Command.rPush key values = { request := LeanRedis.CommandRequest.rPush key values, decode := LeanRedis.expectInteger "RPUSH" }

def LeanRedis.Command.lPushX (key value : String) : Command Int

Equations

• LeanRedis.Command.lPushX key value = { request := LeanRedis.CommandRequest.lPushX key value, decode := LeanRedis.expectInteger "LPUSHX" }

def LeanRedis.Command.rPushX (key value : String) : Command Int

Equations

• LeanRedis.Command.rPushX key value = { request := LeanRedis.CommandRequest.rPushX key value, decode := LeanRedis.expectInteger "RPUSHX" }

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

Equations

• LeanRedis.Command.lPop key = { request := LeanRedis.CommandRequest.lPop key, decode := LeanRedis.expectOptionalString "LPOP" }

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

Equations

• LeanRedis.Command.rPop key = { request := LeanRedis.CommandRequest.rPop key, decode := LeanRedis.expectOptionalString "RPOP" }

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

Equations

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

def LeanRedis.Command.lIndex (key : String) (index : Int) : Command (Option String)

Equations

• LeanRedis.Command.lIndex key index = { request := LeanRedis.CommandRequest.lIndex key index, decode := LeanRedis.expectOptionalString "LINDEX" }

def LeanRedis.Command.lRange (key : String) (start stop : Int) : Command (Array String)

Equations

• LeanRedis.Command.lRange key start stop = { request := LeanRedis.CommandRequest.lRange key start stop, decode := LeanRedis.expectPlainStringArray "LRANGE" }

def LeanRedis.Command.lSet (key : String) (index : Int) (value : String) : Command Unit

Equations

• LeanRedis.Command.lSet key index value = { request := LeanRedis.CommandRequest.lSet key index value, decode := LeanRedis.expectOk }

def LeanRedis.Command.lTrim (key : String) (start stop : Int) : Command Unit

Equations

• LeanRedis.Command.lTrim key start stop = { request := LeanRedis.CommandRequest.lTrim key start stop, decode := LeanRedis.expectOk }

def LeanRedis.Command.lRem (key : String) (count : Int) (value : String) : Command Int

Equations

• LeanRedis.Command.lRem key count value = { request := LeanRedis.CommandRequest.lRem key count value, decode := LeanRedis.expectInteger "LREM" }

def LeanRedis.Command.lInsert (key : String) (position : LInsertPosition) (pivot value : String) : Command Int

Equations

• LeanRedis.Command.lInsert key position pivot value = { request := LeanRedis.CommandRequest.lInsert key position pivot value, decode := LeanRedis.expectInteger "LINSERT" }

def LeanRedis.Command.lMove (source destination : String) (fromWhere toWhere : LMoveWhere) : Command (Option String)

Equations

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

def LeanRedis.Command.lPos (key element : String) (options : LPosOptions := { }) : Command (Option Int)

Equations

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

def LeanRedis.Command.lPosMany (key element : String) (options : LPosOptions) : Command (Array Int)

Equations

• LeanRedis.Command.lPosMany key element options = { request := LeanRedis.CommandRequest.lPos key element options, decode := LeanRedis.expectIntegerArray "LPOS" }