[Agda] Agda's syntax declaration

[Martin Escardo]

Can I say some things about Agda's syntax declaration?

* Why are the definitions backwards (what you define is in the
right-hand side)?

* There isn't any precise definition, as far as I know, of the syntax of
syntax.

* And there isn't much documentation, as discussed.

* 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".)

Anyway, after heroic guesswork, I managed to make some useful things to
work nicely using "syntax". (So thanks for implementing this feature!)

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.

:-)

Enjoy the weekend.

Best,
Martin

On 03/11/17 21:51, nad at cse.gu.se wrote:
> On 2017-11-03 16:58, Andrea Vezzosi wrote:
>> 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
> 
> Note that regular list literals have the advantage that there is no need
> to give parentheses around list elements, or around list literals.
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe