<div dir="ltr">The reason syntax declarations are 'backwards' is that they should be read as providing the syntax for a particular identifier. For instance,<div><br></div><div> syntax foo x y z = [ x / y ]- z</div><div><br></div><div>defines the syntax of foo to be the thing on the right. Having it the other way around would give you the wrong idea of what's going on. In particular you'd expect to be able do write things like</div><div><br></div><div> syntax [ x ] = x :: []</div><div><br></div><div>or</div><div><br></div><div> syntax [ x / y ]- z = foo x y z</div><div> syntax [ x /]- z = foo x x z</div><div><br></div><div>The backwards direction doesn't make sense for the telescope syntax though. In that case you are defining a new name (like 'Type' or 'Group') so that should go on the left (in my opinion).</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 27, 2014 at 10:25 AM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">(apparently something got wrong with my previous email, trying again...)</p>
<p dir="ltr">I have no idea why the "syntax" syntax is backwards, but I thought it would make more sense to have both of them backwards rather than having them in different directions.</p>
<div class="gmail_quote">Le 27 nov. 2014 10:21, "Guillaume Brunerie" <<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>> a écrit :<div><div class="h5"><br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It's backwards the same way the current syntax declarations are, and presumably for the same reason.<br>
<br>
> On 26 Nov 2014, at 22:08, Felipe Lessa <<a href="mailto:felipe.lessa@gmail.com" target="_blank">felipe.lessa@gmail.com</a>> wrote:<br>
><br>
> On 26-11-2014 11:33, Guillaume Brunerie wrote:<br>
>> telsyntax {i : Level} (X : Set i) = (X : Type)<br>
><br>
> I hope this isn't an obvious question, but isn't this syntax backwards?<br>
> Shouldn't it be like below?<br>
><br>
> telsyntax (X : Type) = {i : Level} (X : Set i)<br>
><br>
> Cheers, :)<br>
><br>
> --<br>
> Felipe.<br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</blockquote></div></div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>