[Agda] Forget Hurken's Paradox, Agda has a quicker route to success

[Andrés Sicard-Ramírez]

On Thu, Sep 6, 2012 at 12:25 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> I have a fix for this (filed as issue 690), that looks also for occurrences
> in the indices.

FYI, using that fix the following data type (previously accepted) is
rejected by Agda (and Coq)

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

-- 
Andrés