[Agda] Strictly positive types

[Andrés Sicard-Ramírez]

Hi,

Reading in Coq' Art about head type constraints (section 14.1.2.1),
the following type is rejected by Coq 8.4, but it is accepted by Agda
(development version):

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data T : Set → Set where
  c : T (T ℕ)

Could someone explain me the motivation for rejecting the type T in
Coq and/or for accepting it in Agda.

Thanks,

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120820/5852ec35/attachment.html