[Agda] Telescope syntax

[Andy Morris]

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