[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