Parse a list of expressions (typically from a RawApp) into an application.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Concrete.Operators
The parser doesn't know about operators and parses everything as normal
function application. This module contains the functions that parses the
operators properly. For a stand-alone implementation of this see
src/prototyping/mixfix/old.
It also contains the function that puts parenthesis back given the precedence of the context.
Synopsis
- value parseApplication
- value parseArguments
- value parseLHS
- value parsePattern
- value parsePatternSyn
- PackageAgda-2.8.0.2
- Exports5
- LanguageHaskell2010
- LicenceMIT
- SourceOperators.hs
value
parseArguments Parse the arguments of a raw application with known head.
value
parseLHS :: DisplayLHSAre we parsing a DisplayPragma?
-> QNameName of the definition.
-> PatternFull left hand side.
-> ScopeM LHSCore
Parses a left-hand side, and makes sure that it defined the expected name.
Parses a pattern.