<div dir="ltr">The reason syntax declarations are &#39;backwards&#39; 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&#39;s going on. In particular you&#39;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&#39;t make sense for the telescope syntax though. In that case you are defining a new name (like &#39;Type&#39; or &#39;Group&#39;) 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">&lt;<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>&gt;</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 &quot;syntax&quot; 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, &quot;Guillaume Brunerie&quot; &lt;<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>&gt; 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&#39;s backwards the same way the current syntax declarations are, and presumably for the same reason.<br>
<br>
&gt; On 26 Nov 2014, at 22:08, Felipe Lessa &lt;<a href="mailto:felipe.lessa@gmail.com" target="_blank">felipe.lessa@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; On 26-11-2014 11:33, Guillaume Brunerie wrote:<br>
&gt;&gt;  telsyntax {i : Level} (X : Set i) = (X : Type)<br>
&gt;<br>
&gt; I hope this isn&#39;t an obvious question, but isn&#39;t this syntax backwards?<br>
&gt; Shouldn&#39;t it be like below?<br>
&gt;<br>
&gt;  telsyntax (X : Type) = {i : Level} (X : Set i)<br>
&gt;<br>
&gt; Cheers, :)<br>
&gt;<br>
&gt; --<br>
&gt; Felipe.<br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt; <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>