[Agda] syntax declaration

[Philip Wadler]

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


Please don't! Relying on a difference that no one can see is bound to lead
to problems. There are many colon-like symbols that are easy to distinguish
from a colon, see here:

    https://unicode-search.net/unicode-namesearch.pl?term=COLON

My favourite is:

U+2982 ⦂ e2 a6 82 Z NOTATION TYPE *COLON*

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Mon, 23 Mar 2020 at 14:25, a.j.rouvoet <a.j.rouvoet at gmail.com> wrote:

> 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 ?
> >>>
> >>
> >
> _______________________________________________
> 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/e87f6b2c/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200323/e87f6b2c/attachment.ksh>