def LeanRedis.expectOk (reply : Protocol.Resp.Value) : Except Error Unit

Equations

• LeanRedis.expectOk (LeanRedis.Protocol.Resp.Value.simpleString "OK") = pure ()
• LeanRedis.expectOk (LeanRedis.Protocol.Resp.Value.blobString bytes) = match String.fromUTF8? bytes with | some "OK" => pure () | x => throw (LeanRedis.Error.decode "expected OK reply")
• LeanRedis.expectOk (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectOk reply = throw (LeanRedis.Error.decode "expected OK reply")

def LeanRedis.expectPong (reply : Protocol.Resp.Value) : Except Error (Option String)

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.expectPong (LeanRedis.Protocol.Resp.Value.simpleString "PONG") = pure none
• LeanRedis.expectPong (LeanRedis.Protocol.Resp.Value.simpleString text) = pure (some text)
• LeanRedis.expectPong (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectPong reply = throw (LeanRedis.Error.decode "unexpected PING reply")

def LeanRedis.expectStored (reply : Protocol.Resp.Value) : Except Error Bool

Equations

• LeanRedis.expectStored (LeanRedis.Protocol.Resp.Value.simpleString "OK") = pure true
• LeanRedis.expectStored (LeanRedis.Protocol.Resp.Value.blobString bytes) = match String.fromUTF8? bytes with | some "OK" => pure true | x => throw (LeanRedis.Error.decode "expected OK reply")
• LeanRedis.expectStored LeanRedis.Protocol.Resp.Value.null = pure false
• LeanRedis.expectStored (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectStored reply = throw (LeanRedis.Error.decode "unexpected SET reply")

def LeanRedis.decodeUtf8 (context : String) (bytes : ByteArray) : Except Error String

Equations

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

def LeanRedis.expectOptionalString (context : String) (reply : Protocol.Resp.Value) : Except Error (Option String)

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.expectOptionalString context LeanRedis.Protocol.Resp.Value.null = pure none
• LeanRedis.expectOptionalString context (LeanRedis.Protocol.Resp.Value.simpleString text) = pure (some text)
• LeanRedis.expectOptionalString context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectOptionalString context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectString (context : String) (reply : Protocol.Resp.Value) : Except Error String

Equations

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

def LeanRedis.expectInteger (context : String) (reply : Protocol.Resp.Value) : Except Error Int

Equations

• LeanRedis.expectInteger context (LeanRedis.Protocol.Resp.Value.number value) = pure value
• LeanRedis.expectInteger context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectInteger context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectBoolean (context : String) (reply : Protocol.Resp.Value) : Except Error Bool

Equations

• LeanRedis.expectBoolean context (LeanRedis.Protocol.Resp.Value.bool value) = pure value
• LeanRedis.expectBoolean context (LeanRedis.Protocol.Resp.Value.number value) = pure (value != 0)
• LeanRedis.expectBoolean context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectBoolean context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectStringArray (context : String) (reply : Protocol.Resp.Value) : Except Error (Array (Option String))

Equations

• LeanRedis.expectStringArray context (LeanRedis.Protocol.Resp.Value.array items) = Array.mapM (LeanRedis.expectOptionalString context) items
• LeanRedis.expectStringArray context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectStringArray context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectPlainStringArray (context : String) (reply : Protocol.Resp.Value) : Except Error (Array String)

Equations

• LeanRedis.expectPlainStringArray context (LeanRedis.Protocol.Resp.Value.array items) = Array.mapM (LeanRedis.expectString context) items
• LeanRedis.expectPlainStringArray context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectPlainStringArray context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectIntegerArray (context : String) (reply : Protocol.Resp.Value) : Except Error (Array Int)

Equations

• LeanRedis.expectIntegerArray context (LeanRedis.Protocol.Resp.Value.array items) = Array.mapM (LeanRedis.expectInteger context) items
• LeanRedis.expectIntegerArray context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectIntegerArray context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.decodeStringPairsFromArray (context : String) (items : Array Protocol.Resp.Value) : Except Error (Array (String × String))

Equations

• LeanRedis.decodeStringPairsFromArray context items = LeanRedis.decodeStringPairsFromArray.loop context items 0 #[]

@[irreducible]

def LeanRedis.decodeStringPairsFromArray.loop (context : String) (items : Array Protocol.Resp.Value) (index : Nat) (acc : Array (String × String)) : Except Error (Array (String × String))

Equations

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

def LeanRedis.expectStringPairs (context : String) (reply : Protocol.Resp.Value) : Except Error (Array (String × String))

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.expectStringPairs context (LeanRedis.Protocol.Resp.Value.array items) = LeanRedis.decodeStringPairsFromArray context items
• LeanRedis.expectStringPairs context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectStringPairs context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectHScanResult (reply : Protocol.Resp.Value) : Except Error HashScanResult

Equations

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

def LeanRedis.expectSetScanResult (reply : Protocol.Resp.Value) : Except Error SetScanResult

Equations

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

def LeanRedis.expectScanResult (reply : Protocol.Resp.Value) : Except Error ScanResult

Equations

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

def LeanRedis.expectOptionalStringOrArray (context : String) (reply : Protocol.Resp.Value) : Except Error (Option String ⊕ Array String)

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.expectOptionalStringOrArray context LeanRedis.Protocol.Resp.Value.null = pure (Sum.inl none)
• LeanRedis.expectOptionalStringOrArray context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectOptionalStringOrArray context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.decodeSortedSetEntriesFromArray (context : String) (items : Array Protocol.Resp.Value) : Except Error (Array SortedSetEntry)

Equations

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

def LeanRedis.expectSortedSetEntries (context : String) (reply : Protocol.Resp.Value) : Except Error (Array SortedSetEntry)

Equations

• One or more equations did not get rendered due to their size.
• LeanRedis.expectSortedSetEntries context (LeanRedis.Protocol.Resp.Value.array items) = LeanRedis.decodeSortedSetEntriesFromArray context items
• LeanRedis.expectSortedSetEntries context (LeanRedis.Protocol.Resp.Value.simpleError message) = throw (LeanRedis.Error.server message)
• LeanRedis.expectSortedSetEntries context reply = throw (LeanRedis.Error.decode (toString "unexpected " ++ toString context ++ toString " reply"))

def LeanRedis.expectSortedSetScanResult (reply : Protocol.Resp.Value) : Except Error SortedSetScanResult

Equations

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