[Agda] syntax declaration

Michel Levy michel.levy.imag at free.fr
Mon Mar 23 17:53:13 CET 2020


I made the following statement

data exists (A : Set)(P : A -> Set): Set where
  <_,_> : (a : A) -> P a -> exists A P

I would like to rewrite (exists A P) as, for example,  (ex (x : A) P x).
But I don't understand how to do it. I tried :

syntax exists A P   = ex  (x : A) , P x

but I had the mistake : syntax must use holes exactly once

Can you explain to me how to use the syntax declaration on this example ? What are these holes in my syntax statement ?

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr


More information about the Agda mailing list