[Agda] syntax declaration

[Michel Levy]

My apologies to Philip Walder and Martin Escardo: they were right but I
didn't understand them.
Below, I give an example of a short module using their suggestion.

module syntax-exists where

data exists (A : Set)(P : A -> Set): Set where
  <_,_> : (a : A) -> P a -> exists A P
 
syntax exists A (\ x -> B ) = ex x ꞉ A ,  B
-- The colon is NOT the usual one (reserved by agda) but obtained by
-- the combination Alt Gr \, : ,4, RET
-- Actually, you can used any sign not reserved by agda.
-- The syntax declaration means, if P is (\ x -> B) then you can use (ex
x : A, B) as a
-- notation for (exists A P)

-- My first theorem with this new syntax :  (P a) -> (ex x ꞉ A, P x)
ex-intro : {A : Set}(a : A)(P : A -> Set) -> (P a) -> (ex x ꞉ A , P x)
ex-intro a P r = < a , r >

-- end of this module

Thank you for your help.
-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr