[Agda] Difference between parameterized and indexed datatypes

v0id_NULL igorzsci at gmail.com
Thu May 4 20:41:32 CEST 2017


Dear list,

Help me please. I can not understand what difference between these
definitions.

data T1 {ℓ} : Set ℓ where
 c1 : T1

data T2 : {ℓ : _} → Set ℓ where
 c2 : T2

Why first one is approved but second one is rejected with error
"The sort of T2 cannot depend on its indices in the type {ℓ :
Agda.Primitive.Level} → Set ℓ when checking the definition of T2"?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170505/bfd05e8f/attachment.html>


More information about the Agda mailing list