[Agda] Telescope syntax

[Felipe Lessa]

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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20141126/af51a673/signature.bin