<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">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">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">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>