[Agda] syntax declaration

[Ulf Norell]

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>
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 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
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
>
> _______________________________________________
> Agda mailing list
> 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/2b1d242b/attachment.html>