[Agda] Termination checking on coinduction

[Alex Rozenshteyn]

Thank you!

On Fri, Feb 17, 2012 at 8:09 AM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> 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
>



-- 
          Alex R