def LeanRedis.Protocol.Resp.Encode.crlf : String

Equations

• LeanRedis.Protocol.Resp.Encode.crlf = "\x0d\n"

def LeanRedis.Protocol.Resp.Encode.encodeBulkString (arg : ByteArray) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeBulkString arg = (("$" ++ toString arg.size ++ LeanRedis.Protocol.Resp.Encode.crlf).toUTF8.append arg).append LeanRedis.Protocol.Resp.Encode.crlf.toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeArrayHeader (count : Nat) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeArrayHeader count = (toString "*" ++ toString count ++ toString LeanRedis.Protocol.Resp.Encode.crlf).toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeSetHeader (count : Nat) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeSetHeader count = (toString "~" ++ toString count ++ toString LeanRedis.Protocol.Resp.Encode.crlf).toUTF8

def LeanRedis.Protocol.Resp.Encode.encodePushHeader (count : Nat) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodePushHeader count = (toString ">" ++ toString count ++ toString LeanRedis.Protocol.Resp.Encode.crlf).toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeMapHeader (count : Nat) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeMapHeader count = (toString "%" ++ toString count ++ toString LeanRedis.Protocol.Resp.Encode.crlf).toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeTextLine (tag value : String) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeTextLine tag value = (tag ++ value ++ LeanRedis.Protocol.Resp.Encode.crlf).toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeBlobWithPrefix (tag : String) (bytes : ByteArray) : ByteArray

Equations

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

partial def LeanRedis.Protocol.Resp.Encode.encodeValue : Value → ByteArray

def LeanRedis.Protocol.Resp.Encode.encodeCommandName (name : String) : ByteArray

Equations

• LeanRedis.Protocol.Resp.Encode.encodeCommandName name = LeanRedis.Protocol.Resp.Encode.encodeBulkString name.toUTF8

def LeanRedis.Protocol.Resp.Encode.encodeCommand (request : CommandRequest) : Array ByteArray

Equations

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