instance Std.Internal.Parsec.String.instInputIteratorCharPos : Std.Internal.Parsec.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

Equations

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

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

Equations

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

def Std.Internal.Parsec.String.pstring (s : String) : Std.Internal.Parsec.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) : Std.Internal.Parsec.String.Parser Unit

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

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) : Std.Internal.Parsec.String.Parser String

Equations

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