<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">guillaume.brunerie@gmail.com</a>> 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'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>