instance Std.Internal.Parsec.String.instInputIteratorCharPos : Input String.Iterator Char String.Pos

Equations

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

@[reducible, inline]

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

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

Equations

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

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

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

Equations

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

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

Parses the given string.

Equations

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

@[inline]

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

Skips the given string.

Equations

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

@[inline]

def Std.Internal.Parsec.String.pchar (c : Char) : Parser Char

Parses the given char.

Equations

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

@[inline]

def Std.Internal.Parsec.String.skipChar (c : Char) : Parser Unit

Skips the given char.

Equations

• Std.Internal.Parsec.String.skipChar c = Std.Internal.Parsec.String.pchar c *> pure ()

@[inline]

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

Parse an ASCII digit 0-9 as a Char.

Equations

• Std.Internal.Parsec.String.digit = (do let c ← Std.Internal.Parsec.any if '0' ≤ c ∧ c ≤ '9' then pure c else Std.Internal.Parsec.fail (toString "digit expected")).attempt

@[inline]

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

Parse one or more ASCII digits into a Nat.

Equations

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

@[inline]

def Std.Internal.Parsec.String.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.String.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.String.ws : Parser Unit

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

Equations

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

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

Takes a fixed amount of chars from the iterator.

Equations

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