[Agda] Problem with coinduction and positivity checker

[Nils Anders Danielsson]

On 2010-01-25 14:49, Andreas Abel wrote:
> codata is still experimental in Agda, even more so data with \infty as 
> \omegaChain below.

I would say that ∞ is at most as experimental as codata; ∞ is
(currently) defined using codata.

-- 
/NAD