[Agda] Telescope syntax

[Guillaume Brunerie]

>
> 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/bc316f98/attachment.html