inductive LeanRedis.Expiration : Type

• ex (seconds : UInt64) : Expiration
• px (milliseconds : UInt64) : Expiration
• exAt (unixSeconds : UInt64) : Expiration
• pxAt (unixMilliseconds : UInt64) : Expiration

@[implicit_reducible]

instance LeanRedis.instBEqExpiration : BEq Expiration

Equations

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

def LeanRedis.instBEqExpiration.beq : Expiration → Expiration → Bool

Equations

• LeanRedis.instBEqExpiration.beq (LeanRedis.Expiration.ex a) (LeanRedis.Expiration.ex b) = (a == b)
• LeanRedis.instBEqExpiration.beq (LeanRedis.Expiration.px a) (LeanRedis.Expiration.px b) = (a == b)
• LeanRedis.instBEqExpiration.beq (LeanRedis.Expiration.exAt a) (LeanRedis.Expiration.exAt b) = (a == b)
• LeanRedis.instBEqExpiration.beq (LeanRedis.Expiration.pxAt a) (LeanRedis.Expiration.pxAt b) = (a == b)
• LeanRedis.instBEqExpiration.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedExpiration.default : Expiration

Equations

• LeanRedis.instInhabitedExpiration.default = LeanRedis.Expiration.ex default

@[implicit_reducible]

instance LeanRedis.instInhabitedExpiration : Inhabited Expiration

Equations

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

def LeanRedis.instReprExpiration.repr : Expiration → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprExpiration : Repr Expiration

Equations

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

inductive LeanRedis.SetCondition : Type

• nx : SetCondition
• xx : SetCondition

def LeanRedis.instBEqSetCondition.beq : SetCondition → SetCondition → Bool

Equations

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

@[implicit_reducible]

instance LeanRedis.instBEqSetCondition : BEq SetCondition

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedSetCondition : Inhabited SetCondition

Equations

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

def LeanRedis.instInhabitedSetCondition.default : SetCondition

Equations

• LeanRedis.instInhabitedSetCondition.default = LeanRedis.SetCondition.nx

def LeanRedis.instReprSetCondition.repr : SetCondition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprSetCondition : Repr SetCondition

Equations

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

inductive LeanRedis.SetExpiry : Type

• relative (expiration : Expiration) : SetExpiry
• keepTtl : SetExpiry

@[implicit_reducible]

instance LeanRedis.instBEqSetExpiry : BEq SetExpiry

Equations

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

def LeanRedis.instBEqSetExpiry.beq : SetExpiry → SetExpiry → Bool

Equations

• LeanRedis.instBEqSetExpiry.beq (LeanRedis.SetExpiry.relative a) (LeanRedis.SetExpiry.relative b) = (a == b)
• LeanRedis.instBEqSetExpiry.beq LeanRedis.SetExpiry.keepTtl LeanRedis.SetExpiry.keepTtl = true
• LeanRedis.instBEqSetExpiry.beq x✝¹ x✝ = false

def LeanRedis.instInhabitedSetExpiry.default : SetExpiry

Equations

• LeanRedis.instInhabitedSetExpiry.default = LeanRedis.SetExpiry.relative default

@[implicit_reducible]

instance LeanRedis.instInhabitedSetExpiry : Inhabited SetExpiry

Equations

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

@[implicit_reducible]

instance LeanRedis.instReprSetExpiry : Repr SetExpiry

Equations

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

def LeanRedis.instReprSetExpiry.repr : SetExpiry → Nat → Std.Format

Equations

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

structure LeanRedis.SetOptions : Type

• expiry? : Option SetExpiry
• condition? : Option SetCondition

def LeanRedis.instBEqSetOptions.beq : SetOptions → SetOptions → Bool

Equations

• LeanRedis.instBEqSetOptions.beq { expiry? := a, condition? := a_1 } { expiry? := b, condition? := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqSetOptions.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqSetOptions : BEq SetOptions

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedSetOptions : Inhabited SetOptions

Equations

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

def LeanRedis.instInhabitedSetOptions.default : SetOptions

Equations

• LeanRedis.instInhabitedSetOptions.default = { expiry? := default, condition? := default }

@[implicit_reducible]

instance LeanRedis.instReprSetOptions : Repr SetOptions

Equations

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

def LeanRedis.instReprSetOptions.repr : SetOptions → Nat → Std.Format

Equations

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

inductive LeanRedis.GetExMode : Type

• relative (expiration : Expiration) : GetExMode
• persist : GetExMode

def LeanRedis.instBEqGetExMode.beq : GetExMode → GetExMode → Bool

Equations

• LeanRedis.instBEqGetExMode.beq (LeanRedis.GetExMode.relative a) (LeanRedis.GetExMode.relative b) = (a == b)
• LeanRedis.instBEqGetExMode.beq LeanRedis.GetExMode.persist LeanRedis.GetExMode.persist = true
• LeanRedis.instBEqGetExMode.beq x✝¹ x✝ = false

@[implicit_reducible]

instance LeanRedis.instBEqGetExMode : BEq GetExMode

Equations

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

@[implicit_reducible]

instance LeanRedis.instInhabitedGetExMode : Inhabited GetExMode

Equations

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

def LeanRedis.instInhabitedGetExMode.default : GetExMode

Equations

• LeanRedis.instInhabitedGetExMode.default = LeanRedis.GetExMode.relative default

@[implicit_reducible]

instance LeanRedis.instReprGetExMode : Repr GetExMode

Equations

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

def LeanRedis.instReprGetExMode.repr : GetExMode → Nat → Std.Format

Equations

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

def LeanRedis.CommandRequest.expirationArgs (expiration : Expiration) : Array ByteArray

Equations

• LeanRedis.CommandRequest.expirationArgs (LeanRedis.Expiration.ex a) = LeanRedis.CommandRequest.utf8Args #["EX", toString a]
• LeanRedis.CommandRequest.expirationArgs (LeanRedis.Expiration.px a) = LeanRedis.CommandRequest.utf8Args #["PX", toString a]
• LeanRedis.CommandRequest.expirationArgs (LeanRedis.Expiration.exAt a) = LeanRedis.CommandRequest.utf8Args #["EXAT", toString a]
• LeanRedis.CommandRequest.expirationArgs (LeanRedis.Expiration.pxAt a) = LeanRedis.CommandRequest.utf8Args #["PXAT", toString a]

def LeanRedis.CommandRequest.setExpiryArgs (expiry : SetExpiry) : Array ByteArray

Equations

• LeanRedis.CommandRequest.setExpiryArgs (LeanRedis.SetExpiry.relative a) = LeanRedis.CommandRequest.expirationArgs a
• LeanRedis.CommandRequest.setExpiryArgs LeanRedis.SetExpiry.keepTtl = LeanRedis.CommandRequest.utf8Args #["KEEPTTL"]

def LeanRedis.CommandRequest.conditionArgs (condition : SetCondition) : Array ByteArray

Equations

• LeanRedis.CommandRequest.conditionArgs LeanRedis.SetCondition.nx = LeanRedis.CommandRequest.utf8Args #["NX"]
• LeanRedis.CommandRequest.conditionArgs LeanRedis.SetCondition.xx = LeanRedis.CommandRequest.utf8Args #["XX"]

def LeanRedis.CommandRequest.getExModeArgs (mode : GetExMode) : Array ByteArray

Equations

• LeanRedis.CommandRequest.getExModeArgs (LeanRedis.GetExMode.relative a) = LeanRedis.CommandRequest.expirationArgs a
• LeanRedis.CommandRequest.getExModeArgs LeanRedis.GetExMode.persist = LeanRedis.CommandRequest.utf8Args #["PERSIST"]

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

GET key

Equations

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

def LeanRedis.CommandRequest.set (key value : String) (options : SetOptions := { }) : CommandRequest

SET key value [NX | XX] [EX seconds | PX milliseconds | EXAT unix-time-seconds | PXAT unix-time-milliseconds | KEEPTTL]

Equations

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

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

MGET key [key ...]

Equations

• LeanRedis.CommandRequest.mGet keys = { name := "MGET", args := LeanRedis.CommandRequest.utf8Args keys }

def LeanRedis.CommandRequest.mSet (entries : Array (String × String)) : CommandRequest

MSET key value [key value ...]

Equations

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

def LeanRedis.CommandRequest.mSetNx (entries : Array (String × String)) : CommandRequest

MSETNX key value [key value ...]

Equations

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

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

GETDEL key

Equations

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

def LeanRedis.CommandRequest.getEx (key : String) (mode? : Option GetExMode := none) : CommandRequest

GETEX key [EX seconds | PX milliseconds | EXAT unix-time-seconds | PXAT unix-time-milliseconds | PERSIST]

Equations

• LeanRedis.CommandRequest.getEx key (some mode) = { name := "GETEX", args := LeanRedis.CommandRequest.utf8Args #[key] ++ LeanRedis.CommandRequest.getExModeArgs mode }
• LeanRedis.CommandRequest.getEx key = { name := "GETEX", args := LeanRedis.CommandRequest.utf8Args #[key] ++ #[] }

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

GETRANGE key start end

Equations

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

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

GETSET key value

Equations

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

def LeanRedis.CommandRequest.setRange (key : String) (offset : UInt64) (value : String) : CommandRequest

SETRANGE key offset value

Equations

• LeanRedis.CommandRequest.setRange key offset value = { name := "SETRANGE", args := LeanRedis.CommandRequest.utf8Args #[key, toString offset, value] }

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

STRLEN key

Equations

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

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

APPEND key value

Equations

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

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

INCR key

Equations

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

def LeanRedis.CommandRequest.incrBy (key : String) (amount : Int) : CommandRequest

INCRBY key increment

Equations

• LeanRedis.CommandRequest.incrBy key amount = { name := "INCRBY", args := LeanRedis.CommandRequest.utf8Args #[key, toString amount] }

def LeanRedis.CommandRequest.incrByFloat (key amount : String) : CommandRequest

INCRBYFLOAT key increment

Equations

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

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

DECR key

Equations

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

def LeanRedis.CommandRequest.decrBy (key : String) (amount : Int) : CommandRequest

DECRBY key decrement

Equations

• LeanRedis.CommandRequest.decrBy key amount = { name := "DECRBY", args := LeanRedis.CommandRequest.utf8Args #[key, toString amount] }

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

SETNX key value

Equations

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

def LeanRedis.CommandRequest.setEx (key : String) (seconds : UInt64) (value : String) : CommandRequest

SETEX key seconds value

Equations

• LeanRedis.CommandRequest.setEx key seconds value = { name := "SETEX", args := LeanRedis.CommandRequest.utf8Args #[key, toString seconds, value] }

def LeanRedis.CommandRequest.pSetEx (key : String) (milliseconds : UInt64) (value : String) : CommandRequest

PSETEX key milliseconds value

Equations

• LeanRedis.CommandRequest.pSetEx key milliseconds value = { name := "PSETEX", args := LeanRedis.CommandRequest.utf8Args #[key, toString milliseconds, value] }

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

Equations

• LeanRedis.Command.get key = { request := LeanRedis.CommandRequest.get key, decode := LeanRedis.expectOptionalString "GET" }

def LeanRedis.Command.set (key value : String) (options : SetOptions := { }) : Command Bool

Equations

• LeanRedis.Command.set key value options = { request := LeanRedis.CommandRequest.set key value options, decode := LeanRedis.expectStored }

def LeanRedis.Command.mGet (keys : Array String) : Command (Array (Option String))

Equations

• LeanRedis.Command.mGet keys = { request := LeanRedis.CommandRequest.mGet keys, decode := LeanRedis.expectStringArray "MGET" }

def LeanRedis.Command.mSet (entries : Array (String × String)) : Command Unit

Equations

• LeanRedis.Command.mSet entries = { request := LeanRedis.CommandRequest.mSet entries, decode := LeanRedis.expectOk }

def LeanRedis.Command.mSetNx (entries : Array (String × String)) : Command Bool

Equations

• LeanRedis.Command.mSetNx entries = { request := LeanRedis.CommandRequest.mSetNx entries, decode := LeanRedis.expectBoolean "MSETNX" }

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

Equations

• LeanRedis.Command.getDel key = { request := LeanRedis.CommandRequest.getDel key, decode := LeanRedis.expectOptionalString "GETDEL" }

def LeanRedis.Command.getEx (key : String) (mode? : Option GetExMode := none) : Command (Option String)

Equations

• LeanRedis.Command.getEx key mode? = { request := LeanRedis.CommandRequest.getEx key mode?, decode := LeanRedis.expectOptionalString "GETEX" }

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

Equations

• LeanRedis.Command.getRange key start stop = { request := LeanRedis.CommandRequest.getRange key start stop, decode := LeanRedis.expectString "GETRANGE" }

def LeanRedis.Command.getSet (key value : String) : Command (Option String)

Equations

• LeanRedis.Command.getSet key value = { request := LeanRedis.CommandRequest.getSet key value, decode := LeanRedis.expectOptionalString "GETSET" }

def LeanRedis.Command.setRange (key : String) (offset : UInt64) (value : String) : Command Int

Equations

• LeanRedis.Command.setRange key offset value = { request := LeanRedis.CommandRequest.setRange key offset value, decode := LeanRedis.expectInteger "SETRANGE" }

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

Equations

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

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

Equations

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

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

Equations

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

def LeanRedis.Command.incrBy (key : String) (amount : Int) : Command Int

Equations

• LeanRedis.Command.incrBy key amount = { request := LeanRedis.CommandRequest.incrBy key amount, decode := LeanRedis.expectInteger "INCRBY" }

def LeanRedis.Command.incrByFloat (key amount : String) : Command String

Equations

• LeanRedis.Command.incrByFloat key amount = { request := LeanRedis.CommandRequest.incrByFloat key amount, decode := LeanRedis.expectString "INCRBYFLOAT" }

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

Equations

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

def LeanRedis.Command.decrBy (key : String) (amount : Int) : Command Int

Equations

• LeanRedis.Command.decrBy key amount = { request := LeanRedis.CommandRequest.decrBy key amount, decode := LeanRedis.expectInteger "DECRBY" }

def LeanRedis.Command.setNx (key value : String) : Command Bool

Equations

• LeanRedis.Command.setNx key value = { request := LeanRedis.CommandRequest.setNx key value, decode := LeanRedis.expectBoolean "SETNX" }

def LeanRedis.Command.setEx (key : String) (seconds : UInt64) (value : String) : Command Unit

Equations

• LeanRedis.Command.setEx key seconds value = { request := LeanRedis.CommandRequest.setEx key seconds value, decode := LeanRedis.expectOk }

def LeanRedis.Command.pSetEx (key : String) (milliseconds : UInt64) (value : String) : Command Unit

Equations

• LeanRedis.Command.pSetEx key milliseconds value = { request := LeanRedis.CommandRequest.pSetEx key milliseconds value, decode := LeanRedis.expectOk }