[Agda] Simple Agda Libraries

[Nils Anders Danielsson]

On 2009-01-12 11:32, Lennart Augustsson wrote:
>
> Actually, I find mixfix operators much more complex to parse when
> reading code. But as with all custom syntax, when used correctly they
> can also make it much easier to read.

I agree that it is easy to abuse mixfix operators (and infix operators
as well). However, my gut feeling is that lexical issues may be more
important than the added complexity of the grammar; Agda makes it quite
hard to distinguish operators and non-operators. In "Parsing distfix
operators" Simon Peyton Jones suggests annotating the different parts of
a mixfix operator lexically:

   if` ... `then` ... `else` ...

We could provide something like that through the syntax highlighting
mechanism. Do you think that it would make parsing mixfix operators
easier?

It is already possible to highlight operators differently from
non-operators, for instance by underlining them or using a different
background colour, but I have not turned on this by default because I
think it looks annoying. If people disagree then I can change the
defaults, though.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.