|
Agda.Syntax.Concrete.Operators |
|
|
Description |
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.
It also contains the function that puts parenthesis back given the
precedence of the context.
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
Parses a left-hand side, and makes sure that it defined the expected name.
TODO: check the arities of constructors. There is a possible ambiguity with
postfix constructors:
Assume _ * is a constructor. Then 'true *' can be parsed as either the
intended _* applied to true, or as true applied to a variable *. If we
check arities this problem won't appear.
|
|
|
|
|
|
Produced by Haddock version 2.6.1 |