[Agda] Agda's syntax declaration

[Ulf Norell]

On Mon, Nov 6, 2017 at 10:08 AM, Andreas Abel <abela at chalmers.se> wrote:

> I must say I am with Martin on this.  I never understood why the syntax
> declarations are backwards.  The usual mathematical style is that you
> introduce a notation and what it expands to.  It is the notation which is
> the new thing and whose meaning is defined in terms of things understood
> before, and the defined thing is commonly on the left hand side of the =.
>
> And Ulf, your explanation is very implementation-centric.


Indeed, my explanation was of what's actually implemented in Agda at the
moment. One can certainly imagine other syntax extension mechanisms that
may or may not be easier to grasp for a user.

I'm still not sure why the "parsing rule" intuition doesn't work for you.
No one writes grammars with the new syntax in the left-hand side.

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