@[reducible, inline]

abbrev LeanRedis.CommandRequest.ping (message? : Option String := none) : CommandRequest

PING [message]

Equations

• LeanRedis.CommandRequest.ping (some message) = { name := "PING", args := #[message.toUTF8] }
• LeanRedis.CommandRequest.ping = { name := "PING" }

@[reducible, inline]

abbrev LeanRedis.Command.ping (message? : Option String := none) : Command (Option String)

Equations

• LeanRedis.Command.ping message? = { request := LeanRedis.CommandRequest.ping message?, decode := LeanRedis.expectPong }

@[reducible, inline]

abbrev LeanRedis.CommandRequest.auth (auth : AuthConfig) : CommandRequest

AUTH [username] password

Equations

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

@[reducible, inline]

abbrev LeanRedis.Command.auth (auth : AuthConfig) : Command Unit

Equations

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

@[reducible, inline]

abbrev LeanRedis.CommandRequest.select (database : UInt32) : CommandRequest

SELECT index

Equations

• LeanRedis.CommandRequest.select database = { name := "SELECT", args := #[(toString database).toUTF8] }

@[reducible, inline]

abbrev LeanRedis.Command.select (database : UInt32) : Command Unit

Equations

• LeanRedis.Command.select database = { request := LeanRedis.CommandRequest.select database, decode := LeanRedis.expectOk }

def LeanRedis.CommandRequest.selectedDb? (request : CommandRequest) : Option UInt32

Equations

• request.selectedDb? = do guard ((request.name == "SELECT") = true) let bytes ← request.args[0]? let text ← String.fromUTF8? bytes let value ← text.toNat? pure value.toUInt32