Parse a module.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Parser.Parser
The parser is generated by Happy (http://www.haskell.org/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
- TypeChecking.Rules.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.)
-
Synopsis
- value moduleParser
- value moduleNameParser
- value exprParser
- value exprWhereParser
- value tokensParser
- value holeContentParser
- PackageAgda-2.8.0.2
- Exports6
- LanguageHaskell2010
- LicenceMIT
- SourceParser.hs
Parse an expression. Could be used in interactions.
Parse an expression followed by a where clause. Could be used in interactions.
Parse the token stream. Used by the TeX compiler.