[Agda] Termination checking on coinduction

Alex Rozenshteyn rpglover64 at gmail.com
Fri Feb 17 13:50:52 CET 2012

```I'm relatively new to this, so forgive me if this is something obvious.

The termination checker can't verify that my coinductive function
terminates, but the equivalent inductive function is just fine.
I'd like to know either how I can get the checker to accept my code or
why it's wrong.

Also, any advice for working with coinduction is welcome.

Code below:

------------------------------------------------------------------------------------
module GetMax
where

open import Data.Char
open import Data.Bool
open import Coinduction

open import Data.String hiding (_==_)

isNewline : Char → Bool
isNewline c =  c == '\n'

module SplitColist where
open import Data.Colist
addToListOfLists : {A : Set} -> A -> Colist (Colist A) -> Colist (Colist A)
addToListOfLists x [] = [ [ x ] ]
addToListOfLists x (xs ∷ xss) = (x ∷ ♯ xs) ∷ xss

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

module SplitList where
open import Data.List
addToListOfLists' : {A : Set} -> A -> List (List A) -> List (List A)
addToListOfLists' x [] = [ [ x ] ]
addToListOfLists' x (xs ∷ xss) = (x ∷ xs) ∷ xss

splitList : {A : Set} → (A → Bool) → List A → List (List A)
splitList f [] = [ [] ]
splitList f (x ∷ xs) with f x
... | true = addToListOfLists' x (splitList f xs)
... | false = splitList f xs

------------------------------------------------------------------------------------

Thank you.

--
Alex R
```