[Agda] Agda's coinduction incompatible with initial algebras

[Nils Anders Danielsson]

On 2011-10-04 22:41, Martin Escardo wrote:
> Anyway, can anyone summarize exactly what is going wrong? I am not
> familiar with sized types etc. Can this be explained without too many
> technicalities or need to know "experimental features"?

Thorsten and I wrote a short, somewhat sketchy note about the problems
last year:

   Termination Checking in the Presence of Nested Inductive and
     Coinductive Types
   http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-par2010.html

> Also: what was wrong with the older "codata"?

The current mechanism is a /restriction/ of the older codata, which also
had this problem.

-- 
/NAD