[Agda] Syntax precedences

[Dominique Devriese]

All,

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

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?

Dominique