@[reducible, inline]

abbrev LeanRedis.Protocol.Resp.Parse.Parser (α : Type) : Type

Equations

• LeanRedis.Protocol.Resp.Parse.Parser = Std.Internal.Parsec.ByteArray.Parser

inductive LeanRedis.Protocol.Resp.Parse.ParseStatus (α : Type) : Type

• done {α : Type} (value : α) : ParseStatus α
• needMore {α : Type} : ParseStatus α
• error {α : Type} (message : String) : ParseStatus α

def LeanRedis.Protocol.Resp.Parse.instInhabitedParseStatus.default {a✝ : Type} : ParseStatus a✝

Equations

• LeanRedis.Protocol.Resp.Parse.instInhabitedParseStatus.default = LeanRedis.Protocol.Resp.Parse.ParseStatus.needMore

@[implicit_reducible]

instance LeanRedis.Protocol.Resp.Parse.instInhabitedParseStatus {a✝ : Type} : Inhabited (ParseStatus a✝)

Equations

• LeanRedis.Protocol.Resp.Parse.instInhabitedParseStatus = { default := LeanRedis.Protocol.Resp.Parse.instInhabitedParseStatus.default }

structure LeanRedis.Protocol.Resp.Parse.ParserState : Type

• pending : ByteArray

def LeanRedis.Protocol.Resp.Parse.instInhabitedParserState.default : ParserState

Equations

• LeanRedis.Protocol.Resp.Parse.instInhabitedParserState.default = { pending := default }

@[implicit_reducible]

instance LeanRedis.Protocol.Resp.Parse.instInhabitedParserState : Inhabited ParserState

Equations

• LeanRedis.Protocol.Resp.Parse.instInhabitedParserState = { default := LeanRedis.Protocol.Resp.Parse.instInhabitedParserState.default }

@[reducible, inline]

abbrev LeanRedis.Protocol.Resp.Parse.ParserM (α : Type) : Type

Equations

• LeanRedis.Protocol.Resp.Parse.ParserM = StateT LeanRedis.Protocol.Resp.Parse.ParserState (Except LeanRedis.Error)

def LeanRedis.Protocol.Resp.Parse.cr : UInt8

Equations

• LeanRedis.Protocol.Resp.Parse.cr = '\x0d'.toUInt8

def LeanRedis.Protocol.Resp.Parse.lf : UInt8

Equations

• LeanRedis.Protocol.Resp.Parse.lf = '\n'.toUInt8

def LeanRedis.Protocol.Resp.Parse.decodeUtf8 (bytes : ByteArray) : Except String String

Equations

• LeanRedis.Protocol.Resp.Parse.decodeUtf8 bytes = match String.fromUTF8? bytes with | some text => Except.ok text | none => Except.error "invalid UTF-8 in RESP text payload"

def LeanRedis.Protocol.Resp.Parse.bytesToString (slice : ByteSlice) : Except String String

Equations

• LeanRedis.Protocol.Resp.Parse.bytesToString slice = LeanRedis.Protocol.Resp.Parse.decodeUtf8 slice.toByteArray

def LeanRedis.Protocol.Resp.Parse.parseIntText (text : String) : Except String Int

Equations

• LeanRedis.Protocol.Resp.Parse.parseIntText text = match text.toInt? with | some value => Except.ok value | none => Except.error (toString "invalid integer: " ++ toString text)

def LeanRedis.Protocol.Resp.Parse.parseLineBytes : Parser ByteArray

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseLineText : Parser String

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseVerbatim (bytes : ByteArray) : Value

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseLengthHeader : Parser Int

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseBlobLike (mkValue : ByteArray → Value) : Parser Value

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseBool : Parser Value

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseNumber : Parser Value

Equations

• LeanRedis.Protocol.Resp.Parse.parseNumber = do let __do_lift ← LeanRedis.Protocol.Resp.Parse.parseLengthHeader pure (LeanRedis.Protocol.Resp.Value.number __do_lift)

partial def LeanRedis.Protocol.Resp.Parse.parseArrayLike (mkValue : Array Value → Value) : Parser Value

partial def LeanRedis.Protocol.Resp.Parse.parseMap : Parser Value

partial def LeanRedis.Protocol.Resp.Parse.parseAggregateItems (count : Nat) : Parser (Array Value)

partial def LeanRedis.Protocol.Resp.Parse.parseMapEntries (count : Nat) : Parser (Array (Value × Value))

partial def LeanRedis.Protocol.Resp.Parse.parseValue : Parser Value

def LeanRedis.Protocol.Resp.Parse.feed (state : ParserState) (chunk : ByteArray) : ParserState

Equations

• LeanRedis.Protocol.Resp.Parse.feed state chunk = { pending := state.pending.append chunk }

def LeanRedis.Protocol.Resp.Parse.parseOne (state : ParserState) : ParseStatus (Value × ParserState)

Equations

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

def LeanRedis.Protocol.Resp.Parse.parseAvailable : ParserM (Array Value)

Equations

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