Idris2Doc : Text.Parser

Text.Parser

afterMany : GrammartokTrues -> Grammartokca -> Grammartokca
Parse zero or more instance of `skip` until `p` is encountered,
returning its value.
afterSome : GrammartokTrues -> Grammartokca -> GrammartokTruea
Parse one or more instance of `skip` until `p` is encountered,
returning its value.
between : GrammartokTruel -> Inf (GrammartokTruer) -> Inf (Grammartokca) -> GrammartokTruea
Parse an instance of `p` that is between `left` and `right`.
choice : Foldablet => t (Grammartokca) -> Grammartokca
Try each grammar in a container until the first one succeeds.
Fails if the container is empty.
choiceMap : (a -> Grammartokcb) -> Foldablet => ta -> Grammartokcb
Produce a grammar by applying a function to each element of a container,
then try each resulting grammar until the first one succeeds. Fails if the
container is empty.
choose : Grammartokc1a -> Grammartokc2b -> Grammartok (c1&& Delay c2) (Eitherab)
Try to parse one thing or the other, producing a value that indicates
which option succeeded. If both would succeed, the left option
takes priority.
count : (q : Quantity) -> GrammartokTruea -> Grammartok (isSucc (minq)) (Lista)
Parse `p`, repeated as specified by `q`, returning the list of values.
countExactly : (n : Nat) -> GrammartokTruea -> Grammartok (isSuccn) (Vectna)
Parse `p` `n` times, returning the vector of values.
endBy : GrammartokTrues -> Grammartokca -> GrammartokFalse (Lista)
endBy1 : GrammartokTrues -> Grammartokca -> GrammartokTrue (List1a)
Parse one or more instances of `p`, separated and terminated by `sep`.
many : GrammartokTruea -> GrammartokFalse (Lista)
Parse zero or more things (may match the empty input)
manyTill : Grammartokce -> GrammartokTruea -> Grammartokc (Lista)
Parse zero or more instances of `p` until `end` succeeds, returning the
list of values from `p`. Guaranteed to consume input if `end` consumes.
match : {auto {conArg:433} : (Eqk, TokenKindk)} -> (kind : k) -> Grammar (Tokenk) True (TokTypekind)
Parse a terminal based on a kind of token.
option : a -> Grammartokca -> GrammartokFalsea
Optionally parse a thing, with a default value if the grammar doesn't
match. May match the empty input.
optional : Grammartokca -> GrammartokFalse (Maybea)
Optionally parse a thing.
To provide a default value, use `option` instead.
sepBy : GrammartokTrues -> Grammartokca -> GrammartokFalse (Lista)
Parse zero or more things, each separated by another thing. May
match the empty input.
sepBy1 : GrammartokTrues -> Grammartokca -> Grammartokc (List1a)
Parse one or more things, each separated by another thing.
sepEndBy : GrammartokTrues -> Grammartokca -> GrammartokFalse (Lista)
Parse zero or more instances of `p`, separated by and optionally terminated
by `sep`. Will not match a separator by itself.
sepEndBy1 : GrammartokTrues -> Grammartokca -> Grammartokc (List1a)
Parse one or more instances of `p` separated by and optionally terminated by
`sep`.
some : GrammartokTruea -> GrammartokTrue (List1a)
Parse one or more things
some' : GrammartokTruea -> GrammartokTrue (DPair (Lista) (\xs => NonEmptyxs))
Parse one or more instances of `p`, returning the parsed items and proof
that the resulting list is non-empty.
someTill : Grammartokce -> GrammartokTruea -> GrammartokTrue (List1a)
Parse one or more instances of `p` until `end` succeeds, returning the
list of values from `p`. Guaranteed to consume input.