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

Equations

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

@[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 α.

Equations

• Std.Internal.Parsec.ByteArray.Parser α = Std.Internal.Parsec ByteArray.Iterator α

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.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• Std.Internal.Parsec.ByteArray.skipByte b = Std.Internal.Parsec.ByteArray.pbyte b *> pure ()

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

Skip a sequence of bytes equal to the given ByteArray.

Equations

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

@[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.

Equations

• Std.Internal.Parsec.ByteArray.pstring s = do Std.Internal.Parsec.ByteArray.skipBytes s.toUTF8 pure s

@[inline]

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

Skip a string by matching its UTF-8 bytes.

Equations

• Std.Internal.Parsec.ByteArray.skipString s = Std.Internal.Parsec.ByteArray.pstring s *> pure ()

@[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.

Equations

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

@[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.

Equations

• Std.Internal.Parsec.ByteArray.skipByteChar c = Std.Internal.Parsec.ByteArray.skipByte c.toUInt8

@[inline]

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

Parse an ASCII digit 0-9 as a Char.

Equations

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

@[inline]

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

Parse one or more ASCII digits into a Nat.

Equations

• Std.Internal.Parsec.ByteArray.digits = do let d ← Std.Internal.Parsec.ByteArray.digit Std.Internal.Parsec.ByteArray.digitsCore✝ (Std.Internal.Parsec.ByteArray.digitToNat✝ d.toUInt8)

@[inline]

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

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

Equations

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

@[inline]

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

Parse an octal digit 0-7 as a Char.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• Std.Internal.Parsec.ByteArray.ws it = Std.Internal.Parsec.ParseResult.success (Std.Internal.Parsec.ByteArray.skipWs✝ it) ()

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

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

Equations

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

@[inline]

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

Parses while a predicate is satisfied.

Equations

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

@[inline]

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

Parses until a predicate is satisfied (exclusive).

Equations

• Std.Internal.Parsec.ByteArray.takeUntil pred = Std.Internal.Parsec.ByteArray.takeWhile fun (b : UInt8) => decide ¬pred b = true

@[inline]

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

Skips while a predicate is satisfied.

Equations

• Std.Internal.Parsec.ByteArray.skipWhile pred it = Std.Internal.Parsec.ParseResult.success (Std.Internal.Parsec.ByteArray.skipWhile.findEnd✝ pred 0 it) ()

@[inline]

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

Skips until a predicate is satisfied.

Equations

• Std.Internal.Parsec.ByteArray.skipUntil pred = Std.Internal.Parsec.ByteArray.skipWhile fun (b : UInt8) => decide ¬pred b = true

@[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.

Equations

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

@[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.

Equations

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

@[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.

Equations

• Std.Internal.Parsec.ByteArray.takeUntilUpTo pred limit = Std.Internal.Parsec.ByteArray.takeWhileUpTo (fun (b : UInt8) => decide ¬pred b = true) 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.

Equations

• Std.Internal.Parsec.ByteArray.skipWhileUpTo pred limit it = Std.Internal.Parsec.ParseResult.success (Std.Internal.Parsec.ByteArray.skipWhileUpTo.findEnd✝ pred limit 0 it) ()

@[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.

Equations

• Std.Internal.Parsec.ByteArray.skipUntilUpTo pred limit = Std.Internal.Parsec.ByteArray.skipWhileUpTo (fun (b : UInt8) => decide ¬pred b = true) limit