[Agda] Syntax precedences

[Nils Anders Danielsson]

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?

-- 
/NAD