[Agda] Agda goes coinductive

[Conor McBride]

Hi Andreas

On 6 Jun 2008, at 19:21, Andreas Abel wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Conor,  I completely agree with you, the strategy you have  
> described has
> been implemented by my student Karl Mehltretter in Mugda (MUnich  
> aGDA).

That's good to hear. I'd be interested to see
more details...

> It should be easy to add this to Agda as well.

Does my generativity worry go away somehow? I'm
trying to hack up something with only coconstructors
and unfold to see if I believe it.


>
> On termination checking mutual corecursive definitions:
>
> The basic idea is to treat the output of a corecursive function as an
> additional input for the purpose of termination checking.

[..]

> This extends to mutual recursion using the foetus termination checker,
> which has been spiced up to size-change termination.

Makes a lot of sense.

All the best

Conor