mathlib documentation

core.data.buffer.parser

inductive parse_result  :
Type → Type

def parser  :
Type → Type

The parser monad. If you are familiar with the Parsec library in Haskell, you will understand this.

Equations
def parser.bind {α β : Type} :
parser α(α → parser β)parser β

Equations
def parser.pure {α : Type} :
α → parser α

Equations
def parser.fail {α : Type} :
stringparser α

Equations
@[instance]

Equations
def parser.failure {α : Type} :

Equations
def parser.orelse {α : Type} :
parser αparser αparser α

Equations
@[instance]

Equations
@[instance]
def parser.inhabited {α : Type} :

Equations
def parser.decorate_errors {α : Type} :
thunk (list string)parser αparser α

Overrides the expected token name, and does not consume input on failure.

Equations
def parser.decorate_error {α : Type} :
thunk stringparser αparser α

Overrides the expected token name, and does not consume input on failure.

Equations

Matches a single character. Fails only if there is no more input.

Equations
def parser.sat (p : char → Prop) [decidable_pred p] :

Matches a single character satisfying the given predicate.

Equations

Matches the empty word.

Equations
def parser.ch  :

Matches the given character.

Equations

Matches a whole char_buffer. Does not consume input in case of failure.

Equations

Matches one out of a list of characters.

Equations

Matches a string. Does not consume input in case of failure.

Equations

Number of remaining input characters.

Equations

Matches the end of the input.

Equations
def parser.foldr_core {α β : Type} :
(α → β → β)parser αβ → parser β

Equations
def parser.foldr {α β : Type} :
(α → β → β)parser αβ → parser β

Matches zero or more occurrences of p, and folds the result.

Equations
def parser.foldl_core {α β : Type} :
(α → β → α)α → parser βparser α

Equations
def parser.foldl {α β : Type} :
(α → β → α)α → parser βparser α

Matches zero or more occurrences of p, and folds the result.

Equations
def parser.many {α : Type} :
parser αparser (list α)

Matches zero or more occurrences of p.

Equations
def parser.many' {α : Type} :

Matches zero or more occurrences of p.

Equations
def parser.many1 {α : Type} :
parser αparser (list α)

Matches one or more occurrences of p.

Equations

Matches one or more occurences of the char parser p and implodes them into a string.

Equations
def parser.sep_by1 {α : Type} :
parser unitparser αparser (list α)

Matches one or more occurrences of p, separated by sep.

Equations
def parser.sep_by {α : Type} :
parser unitparser αparser (list α)

Matches zero or more occurrences of p, separated by sep.

Equations
def parser.fix_core {α : Type} :
(parser αparser α)parser α

Equations

Matches a digit (0-9).

Equations

Matches a natural number. Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations
def parser.fix {α : Type} :
(parser αparser α)parser α

Fixpoint combinator satisfying fix F = F (fix F).

Equations

Equations
def parser.run {α : Type} :

Runs a parser on the given input. The parser needs to match the complete input.

Equations
def parser.run_string {α : Type} :
parser αstringstring α

Runs a parser on the given input. The parser needs to match the complete input.

Equations