<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Can I say some things about Agda's syntax declaration?<br>
<br>
* Why are the definitions backwards (what you define is in the<br>
right-hand side)?<br></blockquote><div><br></div><div>They're not. You are defining the syntax for a particular name in the same way that</div><div>you define the value of a particular name (`syntax f x = bla` vs `f x = bla`). If syntax</div><div>declarations were the other way around you would be very surprised to find that you</div><div>can't have multiple syntax declarations for the same name (which you can't).</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">* There isn't any precise definition, as far as I know, of the syntax of<br>
syntax.<br>
<br>
* And there isn't much documentation, as discussed.<br></blockquote><div><br></div><div>What do you feel is missing from the documentation Andrea added [1], aside</div><div>from a more explicit explanation of what you are allowed to write in a syntax</div><div>declaration?</div><div><br></div><div>[1] <a href="http://agda.readthedocs.io/en/latest/language/syntax-declarations.html">http://agda.readthedocs.io/en/latest/language/syntax-declarations.html</a></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
* And it is impossible to google search for "Agda syntax" (say) because<br>
this gives answers about Agda's syntax, and not about the "syntax"<br>
keyword. (And it doesn't help to search for "Agda syntax" or "Agda<br>
syntax keyword" or "Agda syntax declaration".)<br></blockquote><div><br></div><div>Now you can do a page search in the user manual which should work better.</div><div>For future undocumented features your best bet when googling fails is to</div><div>grep the CHANGELOG.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Definitely the most mysterious thing, to make such things work, was to<br>
declare the (polymorphic) identity function as an infix left-associative<br>
operator with priority 0:<br>
<br>
infixl 0 id<br>
<br>
This does work (for some things I've done), but I am not sure how I<br>
figured it out (it is not documented), and I still don't know what<br>
making the identity into an infix left-associative operator means.<br></blockquote><div><br></div><div>You answered this question yourself (and it's explained in the documentation):</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-size:12.8px">This also allows, with the associativity for id (!), to write things such as</span><br style="font-size:12.8px"><span style="font-size:12.8px">   * x ∶ A<br></span><span style="font-size:12.8px">       ∶ A'</span> </blockquote><div><br></div><div>/ Ulf </div></div></div></div>