[Agda] Termination checking on coinduction

[Alex Rozenshteyn]

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