def LeanRedis.Pipeline.ping {α : List Type} (pipeline : Pipeline α) (message? : Option String := none) : Pipeline (α ++ [Option String])

Equations

• pipeline.ping message? = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.ping message?))

def LeanRedis.Pipeline.auth {α : List Type} (pipeline : Pipeline α) (auth : AuthConfig) : Pipeline (α ++ [Unit])

Equations

• pipeline.auth auth = pipeline.hAppend (LeanRedis.Pipeline.fromCommand (LeanRedis.Command.auth auth))

def LeanRedis.Pipeline.select {α : List Type} (pipeline : Pipeline α) (index : UInt32) : Pipeline (α ++ [Unit])

Equations

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