structure LeanRedis.Pipeline (τs : List Type) : Type

• requests : Array CommandRequest
• decode : Nat → Array Protocol.Resp.Value → Except Error (HList τs)

def LeanRedis.Pipeline.length {τs : List Type} : Pipeline τs → Nat

Equations

• x✝.length = x✝¹.length

def LeanRedis.Pipeline.empty : Pipeline []

Equations

• LeanRedis.Pipeline.empty = { requests := #[], decode := fun (x : Nat) (x_1 : Array LeanRedis.Protocol.Resp.Value) => Except.ok HList.nil }

@[implicit_reducible]

instance LeanRedis.Pipeline.instInhabitedNil : Inhabited (Pipeline [])

Equations

• LeanRedis.Pipeline.instInhabitedNil = { default := LeanRedis.Pipeline.empty }

def LeanRedis.Pipeline.fromCommand {α : Type} (cmd : Command α) : Pipeline [α]

Equations

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

def LeanRedis.Pipeline.hAppend {α β : List Type} (p : Pipeline α) (q : Pipeline β) : Pipeline (α ++ β)

Equations

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

@[implicit_reducible]

instance LeanRedis.Pipeline.instHAppendHAppendListType {αs βs : List Type} : HAppend (Pipeline αs) (Pipeline βs) (Pipeline (αs ++ βs))

Equations

• LeanRedis.Pipeline.instHAppendHAppendListType = { hAppend := LeanRedis.Pipeline.hAppend }

def LeanRedis.Pipeline.exec {α : List Type} (pipeline : Pipeline α) (values : Array Protocol.Resp.Value) : Except Error (HList α)

Equations

• pipeline.exec values = pipeline.decode 0 values