ParseError package:Agda

Parse errors: what you get if parsing fails.

Errors that arise at a specific position in the file

Throw a parse error at the current position.

Use parseErrorAt or parseError as appropriate.

Fake a parse error at the specified position. Used, for instance, when lexing nested comments, which when failing will always fail at the end of the file. A more informative position is the beginning of the failing comment.

Report a parse error at the beginning of the given Range'.

The .agda-lib file could not be parsed.

Exceptions thrown by the .agda-lib parser.