[Agda] Agda's syntax declaration

[Ulf Norell]

On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> Can I say some things about Agda's syntax declaration?
>
> * Why are the definitions backwards (what you define is in the
> right-hand side)?
>

They're not. You are defining the syntax for a particular name in the same
way that
you define the value of a particular name (`syntax f x = bla` vs `f x =
bla`). If syntax
declarations were the other way around you would be very surprised to find
that you
can't have multiple syntax declarations for the same name (which you can't).


> * There isn't any precise definition, as far as I know, of the syntax of
> syntax.
>
> * And there isn't much documentation, as discussed.
>

What do you feel is missing from the documentation Andrea added [1], aside
from a more explicit explanation of what you are allowed to write in a
syntax
declaration?

[1] http://agda.readthedocs.io/en/latest/language/syntax-declarations.html


> * And it is impossible to google search for "Agda syntax" (say) because
> this gives answers about Agda's syntax, and not about the "syntax"
> keyword. (And it doesn't help to search for "Agda syntax" or "Agda
> syntax keyword" or "Agda syntax declaration".)
>

Now you can do a page search in the user manual which should work better.
For future undocumented features your best bet when googling fails is to
grep the CHANGELOG.

Definitely the most mysterious thing, to make such things work, was to
> declare the (polymorphic) identity function as an infix left-associative
> operator with priority 0:
>
> infixl 0 id
>
> This does work (for some things I've done), but I am not sure how I
> figured it out (it is not documented), and I still don't know what
> making the identity into an infix left-associative operator means.
>

You answered this question yourself (and it's explained in the
documentation):


> This also allows, with the associativity for id (!), to write things such
> as
>    * x ∶ A
>        ∶ A'


/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171104/feb12772/attachment.html>