<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">guillaume.brunerie@gmail.com</a>&gt; a écrit :<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>