[Agda] Termination checking on coinduction

[Nils Anders Danielsson]

On 2012-02-18 19:40, Alex Rozenshteyn wrote:
> Wouldn't it also be useful to have a function which returns a Costring
> and a proof that it's finite?
>
> That way you'd have a lazy string like in haskell, but you'd be able
> to use it in more ways, right?

If you use the MAlonzo backend, then Strings are represented as Haskell
Strings.

-- 
/NAD