@[implicit_reducible]

instance Std.Internal.Parsec.ByteArray.instInputIteratorUInt8Nat : Input ByteArray.Iterator UInt8 Nat

@[reducible, inline]

abbrev Std.Internal.Parsec.ByteArray.Parser (α : Type) : Type

Parser α is a parser that consumes a ByteArray input using a ByteArray.Iterator and returns a result of type α.

def Std.Internal.Parsec.ByteArray.Parser.run {α : Type} (p : Parser α) (arr : ByteArray) : Except String α

Run a Parser on a ByteArray, returns either the result or an error string with offset.

@[inline]

def Std.Internal.Parsec.ByteArray.pbyte (b : UInt8) : Parser UInt8

Parse a single byte equal to b, fails if different.

@[inline]

def Std.Internal.Parsec.ByteArray.skipByte (b : UInt8) : Parser Unit

Skip a single byte equal to b, fails if different.

def Std.Internal.Parsec.ByteArray.skipBytes (arr : ByteArray) : Parser Unit

Skip a sequence of bytes equal to the given ByteArray.

@[inline]

def Std.Internal.Parsec.ByteArray.pstring (s : String) : Parser String

Parse a string by matching its UTF-8 bytes, returns the string on success.

@[inline]

def Std.Internal.Parsec.ByteArray.skipString (s : String) : Parser Unit

Skip a string by matching its UTF-8 bytes.

@[inline]

def Std.Internal.Parsec.ByteArray.pByteChar (c : Char) : Parser Char

Parse a Char that can be represented in 1 byte. If c uses more than 1 byte it is truncated.

@[inline]

def Std.Internal.Parsec.ByteArray.skipByteChar (c : Char) : Parser Unit

Skip a Char that can be represented in 1 byte. If c uses more than 1 byte it is truncated.

@[inline]

def Std.Internal.Parsec.ByteArray.digit : Parser Char

Parse an ASCII digit 0-9 as a Char.

@[inline]

def Std.Internal.Parsec.ByteArray.digits : Parser Nat

Parse one or more ASCII digits into a Nat.

@[inline]

def Std.Internal.Parsec.ByteArray.hexDigit : Parser Char

Parse a hex digit 0-9, a-f, or A-F as a Char.

@[inline]

def Std.Internal.Parsec.ByteArray.octDigit : Parser Char

Parse an octal digit 0-7 as a Char.

@[inline]

def Std.Internal.Parsec.ByteArray.asciiLetter : Parser Char

Parse an ASCII letter a-z or A-Z as a Char.

@[inline]

def Std.Internal.Parsec.ByteArray.ws : Parser Unit

Skip whitespace: tabs, newlines, carriage returns, and spaces.

def Std.Internal.Parsec.ByteArray.take (n : Nat) : Parser ByteSlice

Parse n bytes from the input into a ByteSlice, errors if not enough bytes.

@[inline]

def Std.Internal.Parsec.ByteArray.takeWhile (pred : UInt8 → Bool) : Parser ByteSlice

Parses while a predicate is satisfied.

@[inline]

def Std.Internal.Parsec.ByteArray.takeUntil (pred : UInt8 → Bool) : Parser ByteSlice

Parses until a predicate is satisfied (exclusive).

@[inline]

def Std.Internal.Parsec.ByteArray.skipWhile (pred : UInt8 → Bool) : Parser Unit

Skips while a predicate is satisfied.

@[inline]

def Std.Internal.Parsec.ByteArray.skipUntil (pred : UInt8 → Bool) : Parser Unit

Skips until a predicate is satisfied.

@[inline]

def Std.Internal.Parsec.ByteArray.takeWhileUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice

Parses while a predicate is satisfied, up to a given limit.

@[inline]

def Std.Internal.Parsec.ByteArray.takeWhileUpTo1 (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice

Parses while a predicate is satisfied, up to a given limit, requiring at least one byte.

@[inline]

def Std.Internal.Parsec.ByteArray.takeUntilUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice

Parses until a predicate is satisfied (exclusive), up to a given limit.

@[inline]

def Std.Internal.Parsec.ByteArray.skipWhileUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser Unit

Skips while a predicate is satisfied, up to a given limit.

@[inline]

def Std.Internal.Parsec.ByteArray.skipUntilUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser Unit

Skips until a predicate is satisfied, up to a given limit.