[Agda] Telescope syntax

[Guillaume Brunerie]

(apparently something got wrong with my previous email, trying again...)

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.
Le 27 nov. 2014 10:21, "Guillaume Brunerie" <guillaume.brunerie at gmail.com>
a écrit :

> It's backwards the same way the current syntax declarations are, and
>> presumably for the same reason.
>>
>> > On 26 Nov 2014, at 22:08, Felipe Lessa <felipe.lessa at gmail.com> wrote:
>> >
>> > On 26-11-2014 11:33, Guillaume Brunerie wrote:
>> >>  telsyntax {i : Level} (X : Set i) = (X : Type)
>> >
>> > I hope this isn't an obvious question, but isn't this syntax backwards?
>> > Shouldn't it be like below?
>> >
>> >  telsyntax (X : Type) = {i : Level} (X : Set i)
>> >
>> > Cheers, :)
>> >
>> > --
>> > Felipe.
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141127/0811bcc4/attachment.html