[Agda] Simple Agda Libraries

[Lennart Augustsson]

I'm not sure how mixfix could be made easier for everyone.
I feel that mixfix helps me when the mixfix operator is just some
syntax that I already know, e.g., the Oxford sematics brackets.  In
this case it helps because the notation is familiar.  But what's
familiar to me can be unfamiliar to someone else, and vice versa.
The beauty about spelling out words is that you can read and get
reminded of their meaning without looking at the definition.  The bad
thing about words is that once you know them they can be in the way of
seeing the bigger picture.
So I don't think there's one right way of doing things that will make
everyone happy.  But I'd advice to use mixfix sparingly when it's some
new notation that is unfamiliar to everyone.

  -- Lennart

On Wed, Jan 14, 2009 at 10:19 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>