[Agda] syntax declaration

[Jason -Zhong Sheng- Hu]

Michel,

why are you using such an old version while reading the doc of a recent one?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Ulf Norell <ulf.norell at gmail.com>
Sent: March 23, 2020 5:49 PM
To: Michel Levy <michel.levy.imag at free.fr>
Cc: Agda users <agda at lists.chalmers.se>
Subject: Re: [Agda] syntax declaration

It should be

syntax exists A (λ x → P) = ex x ∶ A , P

/ Ulf

On Mon, Mar 23, 2020 at 10:13 PM Michel Levy <michel.levy.imag at free.fr<mailto:michel.levy.imag at free.fr>> wrote:
Alas, the suggestion of Martin "syntax exists A P   = ex  x : A , P x"
doesn't work.

I  still have the error : syntax must alternate holes and non-holes.

And I get a lexical error when I replace the colon : by \:4

I  read
"https://agda.readthedocs.io/en/v2.6.0/language/syntax-declarations.html"
without finding the solution.

Remark : I'm using agda version 2.5.3

Le 23/03/2020 à 18:19, Martin Escardo a écrit :
> 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<mailto: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 ?
>>>
>>
>
--
courriel : michel.levy.imag at free.fr<mailto:michel.levy.imag at free.fr>
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr<http://michel.levy.imag.free.fr>

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200323/5d7c4cd7/attachment.html>