[Agda] syntax declaration

[Martin Escardo]

Use a different colon (:) symbol, such as the one you get by typing \:4 
in emacs. I think the normal colon is reserved. Martin

On 23/03/2020 16:53, michel.levy.imag at free.fr wrote:
> 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 ?
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe