[Agda] Syntax precedences

[Jean-Philippe Bernardy]

On Fri, Jun 17, 2011 at 6:36 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-05-31 13:02, Dominique Devriese wrote:
>>
>> I just noticed that syntax declarations for some reason get the lowest
>> associative precedence of all "operators". This allows me to do the
>> following:
>>
>>   open import Data.Empty
>>   syntax ⊥-elim v = impossible: v
>
> This particular code is rejected; syntax declarations must appear
> together with the original definition.
>
>> so that I can do stuff like
>>
>>   postulate A : Set
>>            ¬A : A → ⊥
>>            f : B → A
>>            C : Set
>>
>>   test : B ⊎ C → C
>>   test (inj₁ b) = impossible: ¬A $ f b
>>   test (inj₂ c) = c
>>
>> I find this a nice style, but it seems like a hack..  Any comments?
>
> You can change the fixity of "impossible:" in the following way:
>
>  infix <n> ⊥-elim
>
> I don't know why the default fixity of syntax declarations is different
> from that of ordinary operators. Jean-Philippe, do you?

I think that the default fixity is for syntax declarations is -666. I
used this number to denote the evil hack I've used. What's happenning
is that syntax declarations are another field of fixity declarations.
There is then a function that "mixes" two fixity declarations; and
also checks for conflicts. It does not flag a conflict if one of the
fixities is -666.

Cheers,
JP.