[Agda] Syntax precedences

[Dominique Devriese]

All,

2011/6/17 Nils Anders Danielsson <nad at chalmers.se>:
> 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.

Oh, in my actual code, I indeed have this inside Data.Empty.

>> 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?

As far as I can tell, it's not just the default that is different, but
using syntax, I seem to get a fixity that I cannot specify using a
fixity declaration: strictly lower than the one of _$_, which is 0.

Dominique