[Agda] syntax declaration

[a.j.rouvoet]

Concretely, the following is accepted by Agda:

syntax exists A (λ x -> px) = ex x ∶ A , px

and you can use it as you want (I think):

there-are-numbers-less-than-three : ex x ∶ ℕ , (x ≤ 3)

On 3/23/20 6:19 PM, Martin Escardo wrote:
> Also you will need to write
>
> syntax exists A P   = ex  x : A , P x
>
> without the round brackets, I think.
>
> Martin
>
>
> On 23/03/2020 17:18, Martin Escardo wrote:
>> 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 ?
>>>
>>
>