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.) -

6 values

PackageAgda-2.8.0.2
Exports6
LanguageHaskell2010
LicenceMIT
SourceParser.hs

valuemoduleParser :: Parser Module

Parse a module.

valuemoduleNameParser :: Parser QName

valueexprParser :: Parser Expr

Parse an expression. Could be used in interactions.

valueexprWhereParser :: Parser ExprWhere

Parse an expression followed by a where clause. Could be used in interactions.

valuetokensParser :: Parser [Token]

Parse the token stream. Used by the TeX compiler.

valueholeContentParser :: Parser (HoleContent' () Name Pattern Expr)