[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