[Agda] Termination checking on coinduction

[Nils Anders Danielsson]

On 2012-02-17 13:50, Alex Rozenshteyn wrote:
>    split : {A : Set} → (A → Bool) → Colist A → Colist (Colist A)
>    split f [] = [ [] ]
>    split f (x ∷ xs') with  ♭ xs' | f x
>    ... | xs | true  = addToListOfLists x (split f xs)
>    ... | xs | false = split f xs

This definition is not productive: split (λ _ → false) (repeat unit)
does not produce any output.

Section 2 of the following paper contains an introduction to coinduction
and corecursion in Agda:

   Subtyping, Declaratively
   An Exercise in Mixed Induction and Coinduction
   Myself and Thorsten Altenkirch
   http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping.html

-- 
/NAD