[Agda] Agda's syntax declaration

[Frederik Hanghøj Iversen]

This is really great. Thank you for putting this in the docs. I'll be sure
to search the changelog next time I run into an undocumented feature.

As for the documentation I think this example:

syntax _==_ x y = x === y


Could benefit from a change. As far as I understand it the issue with this
declaration is the LHS, i.e. _==_ and not the RHS ===, but I could be
wrong. So perhaps it's a bit misleading.

Maybe linking the gist for list-syntax would also be helpful (perhaps even
adding it to agda-stdlib?) And the documentation could also expand on the
caveat of using this approach as pointed out by NAD here and Toxaris in the
Gist.

Also, it's a bit funny to me that so many readthedocs articles have the
disclaimer "this is a stub" xD

On Fri, Nov 3, 2017 at 4:58 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Hi Frederik,
>
> it seems like the only documentation was in the CHANGELOG, so I
> collected it here:
>
> https://github.com/agda/agda/blob/master/doc/user-manual/
> language/syntax-declarations.lagda.rst
>
>
> it should soon appear at http://agda.readthedocs.io/ , I presume.
>
> About the list syntax, I was able to find this gist, not sure how well
> it works in practice though.
>
> https://gist.github.com/bishboria/8568581
>
> Cheers,
> Andrea
>
> On Fri, Nov 3, 2017 at 2:06 PM, Frederik Hanghøj Iversen
> <fhi.1990 at gmail.com> wrote:
> > I recently discovered Agda's syntax directive. And just now discovered
> > that as a user I can define my own syntax directive.
> >
> > The thing I'm talking about is exemplified in agda-stdlib in
> Data.Product:
> >
> >     Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
> >     Σ-syntax = Σ
> >
> >     syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
> >
> > Unfortunately I cannot find any documentation on this directive. If
> > anyone has a resource please let me know.
> >
> > I was also wondering if it would be possible to use this directive to
> > define a syntactical construct for e.g. lists with arbitrary elements.
> > That is, I'd like to be able to write a syntax declaration allowing me
> > to write.
> >
> >     [0,1,2]
> >
> > in stead of
> >
> >     0 ∷ 1 ∷ 2 ∷ []
> >
> >
> > Is this possible?
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171104/d54499c6/attachment.html>