mathlib3 documentation

core / data.buffer.parser

inductive parse_result (α : Type) :
Instances for parse_result
  • parse_result.has_sizeof_inst
def parser (α : Type) :

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

Equations
Instances for parser
@[protected]
def parser.bind {α β : Type} (p : parser α) (f : α parser β) :
Equations
@[protected]
def parser.pure {α : Type} (a : α) :
Equations
@[protected]
def parser.fail {α : Type} (msg : string) :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected]
def parser.failure {α : Type} :
Equations
@[protected]
def parser.orelse {α : Type} (p q : parser α) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def parser.inhabited {α : Type} :
Equations
def parser.decorate_errors {α : Type} (msgs : thunk (list string)) (p : parser α) :

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

Equations
Instances for parser.decorate_errors

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

Equations
Instances for parser.any_char
def parser.sat (p : char Prop) [decidable_pred p] :

Matches a single character satisfying the given predicate.

Equations
Instances for parser.sat
def parser.ch (c : char) :

Matches the given character.

Equations
Instances for parser.ch

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

Equations
Instances for parser.char_buf

Matches one out of a list of characters.

Equations
Instances for parser.one_of
def parser.str (s : string) :

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

Equations
Instances for parser.str

Number of remaining input characters.

Equations
Instances for parser.remaining

Matches the end of the input.

Equations
Instances for parser.eof
def parser.foldr_core {α β : Type} (f : α β β) (p : parser α) (b : β) (reps : ) :
Equations
Instances for parser.foldr_core
def parser.foldr {α β : Type} (f : α β β) (p : parser α) (b : β) :

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

Equations
Instances for parser.foldr
def parser.foldl_core {α β : Type} (f : α β α) (a : α) (p : parser β) (reps : ) :
Equations
Instances for parser.foldl_core
def parser.foldl {α β : Type} (f : α β α) (a : α) (p : parser β) :

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

Equations
Instances for parser.foldl
def parser.many {α : Type} (p : parser α) :

Matches zero or more occurrences of p.

Equations
Instances for parser.many
def parser.many' {α : Type} (p : parser α) :

Matches zero or more occurrences of p.

Equations
Instances for parser.many'
def parser.many1 {α : Type} (p : parser α) :

Matches one or more occurrences of p.

Equations
Instances for parser.many1

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

Equations
Instances for parser.many_char1
def parser.sep_by1 {α : Type} (sep : parser unit) (p : parser α) :

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

Equations
Instances for parser.sep_by1
def parser.sep_by {α : Type} (sep : parser unit) (p : parser α) :

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

Equations
Instances for parser.sep_by
def parser.fix_core {α : Type} (F : parser α parser α) (max_depth : ) :
Equations

Matches a digit (0-9).

Equations
Instances for parser.digit

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

Equations
Instances for parser.nat
def parser.fix {α : Type} (F : parser α parser α) :

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

Equations
def parser.mk_error_msg (input : char_buffer) (pos : ) (expected : dlist string) :
Equations
def parser.run {α : Type} (p : parser α) (input : char_buffer) :

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

Equations
def parser.run_string {α : Type} (p : parser α) (input : string) :

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

Equations