<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 6, 2017 at 10:08 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 =.<br>
<br>
And Ulf, your explanation is very implementation-centric.</blockquote><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div>