@[inline]

def Parser.Char.char {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (tk : Char) : ParserT ε σ Char m Char

char tk accepts and returns character tk, otherwise fails

Equations

• Parser.Char.char tk = Parser.withErrorMessage (toString "expected " ++ toString (repr tk) ++ toString "") (Parser.token tk)

def Parser.Char.chars {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (tks : String) : ParserT ε σ Char m String

chars tks accepts and returns string tks, otherwise fails

Equations

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

def Parser.Char.string {ε : Type} {m : Type → Type u_1} [Monad m] [Parser.Error ε Substring Char] (tks : String) : ParserT ε Substring Char m String

string tks accepts and returns string tks, otherwise fails

Equations

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

def Parser.Char.captureStr {ε : Type} {m : Type → Type u_1} [Monad m] {α : Type} [Parser.Error ε Substring Char] (p : ParserT ε Substring Char m α) : ParserT ε Substring Char m (α × Substring)

captureStr p parses p and returns the output of p with the corresponding substring

Equations

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

def Parser.Char.matchStr {ε : Type} {m : Type → Type u_1} [Monad m] [Parser.Error ε Substring Char] (re : RegEx Char) : ParserT ε Substring Char m (Array (Option Substring))

matchStr re accepts and returns substring matches for regex re groups, otherwise fails

Equations

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

@[inline]

def Parser.Char.space {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse space (U+0020)

Equations

• Parser.Char.space = Parser.withErrorMessage "expected space (U+0020)" (Parser.token ' ')

@[inline]

def Parser.Char.tab {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse horizontal tab (U+0009)

Equations

• Parser.Char.tab = Parser.withErrorMessage "expected horizontal tab (U+0009)" (Parser.token '\t')

@[inline]

def Parser.Char.ASCII.lf {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse line feed (U+000A)

Equations

• Parser.Char.ASCII.lf = Parser.withErrorMessage "expected line feed (U+000A)" (Parser.token '\n')

@[inline]

def Parser.Char.ASCII.cr {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse carriage return (U+000D)

Equations

• Parser.Char.ASCII.cr = Parser.withErrorMessage "expected carriage return (U+000D)" (Parser.token '\x0d')

@[inline]

def Parser.Char.eol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse end of line

Equations

• Parser.Char.eol = Parser.withErrorMessage "expected newline" (Parser.Char.ASCII.cr *> Parser.Char.ASCII.lf <|> Parser.Char.ASCII.lf)

def Parser.Char.ASCII.whitespace {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse whitespace character

Equations

• Parser.Char.ASCII.whitespace = Parser.withErrorMessage "expected whitespace character" (Parser.tokenFilter fun (c : Char) => c == ' ' || decide (c ≥ '\t') && decide (c ≤ '\x0d'))

def Parser.Char.ASCII.uppercase {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse uppercase letter character (A..Z)

Equations

• Parser.Char.ASCII.uppercase = Parser.withErrorMessage "expected uppercase letter character" (Parser.tokenFilter fun (c : Char) => decide (c ≥ 'A') && decide (c ≤ 'Z'))

def Parser.Char.ASCII.lowercase {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse lowercase letter character (a..z)

Equations

• Parser.Char.ASCII.lowercase = Parser.withErrorMessage "expected lowercase letter character" (Parser.tokenFilter fun (c : Char) => decide (c ≥ 'a') && decide (c ≤ 'z'))

def Parser.Char.ASCII.alpha {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse alphabetic character (A..Z and a..z)

Equations

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

def Parser.Char.ASCII.numeric {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse numeric character (0..9)

Equations

• Parser.Char.ASCII.numeric = Parser.withErrorMessage "expected decimal digit character" (Parser.tokenFilter fun (c : Char) => decide (c ≥ '0') && decide (c ≤ '9'))

def Parser.Char.ASCII.alphanum {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse alphabetic letter or digit (A..Z, a..z and 0..9)

Equations

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

def Parser.Char.ASCII.control {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

Parse control character

Equations

• Parser.Char.ASCII.control = Parser.withErrorMessage "expected control character" (Parser.tokenFilter fun (c : Char) => decide (c.val < 32) || c.val == 127)

def Parser.Char.ASCII.digit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 10)

Parse decimal digit (0-9)

Equations

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

def Parser.Char.ASCII.binDigit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 2)

Parse binary digit (0..1)

Equations

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

def Parser.Char.ASCII.octDigit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 8)

Parse octal digit (0..7)

Equations

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

def Parser.Char.ASCII.hexDigit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 16)

Parse hexadecimal digit (0..9, A..F and a..f)

Equations

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