The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

Hi,

I don't know about Coq's counterpart of this but this is, I believe, the
standard reference for the parsing of agda's mixfix operators. Notations
may be somewhat related.

http://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.html

Cheers,
--
gallais


On 5 August 2013 22:53, t x 
<txrev319 AT gmail.com>
 wrote:
> Hi,
>
>   I'm currently (past few days, trying to) writing a parser for Coq. With
> the exception of Notation (for which I hard coded the common cases I use)
> and proper handling of precedence (i.e. "1 + 2 * 3" is incorrectly parsed as
> "(1+2)*3"), everything appears to work.
>
>   Courses I had previously take in compilers / automata theory tend to
> assume that the grammar is fixed before the program is compiled. Notation
> breaks this assumption. Can someone explain to me (or point me at a paper)
> on the theoretical foundations behind notation and how it's implemented?
>
> Thanks!