Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



The parser is generated by Happy ( - - Ideally, ranges should be as precise as possible, to get messages that - emphasize precisely the faulting term(s) upon error. - - However, interactive highlighting is only applied at the end of each - mutual block, keywords are only highlighted once (see - Decl). So if the ranges of two declarations - interleave, one must ensure that keyword ranges are not included in - the intersection. (Otherwise they are uncolored by the interactive - highlighting.) -



moduleParser :: Parser ModuleSource

Parse a module.

exprParser :: Parser ExprSource

Parse an expression. Could be used in interactions.

tokensParser :: Parser [Token]Source

Parse the token stream. Used by the TeX compiler.

tests :: IO BoolSource

Test suite.