[Agda] Checking termination is not sufficiently exploratory.

[Serge Leblanc]

Dear all,
Why the checking termination rejects the coSplit" function although the
coSplit' function is accepted ?
Why the checking termination so suspicious?
Sincerely

Estimataj ĉiuj,
Kial la finiĝa kontrolo malakceptas la funkcion coSplit″ kvankam la
funkcio coSplit′ trafas ?
Kial la finiĝa kontrolo estas tiel malakceptanda ?
Sincere

  coSplit′ : Costring → Costring
  coSplit′ [] = []
  coSplit′ (x ∷ xs) with x ≐ '!'
  ... | false = x ∷ ♯ coSplit′ (♭ xs)
  ... | true = '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs))

  coSplit″ : Costring → Costring
  coSplit″ [] = []
  coSplit″ (x ∷ xs) with x ≐ '!'
  ... | false = x ∷ ♯ coSplit″ (♭ xs)
  ... | true = (toCostring ">>") ++ coSplit″ (♭ xs)

  main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘ coSplit′) s

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180730/1751f5f4/attachment.html>
-------------- next part --------------
module EchoInput3 where

  open import IO using (run ; getContents ; _>>=_ ; putStrLn∞)
  open import Coinduction using (♯_ ; ♭)
  open import Function using (_$_ ; _∘_)
  open import Data.Colist as Colist using (Colist ; [] ; _∷_ ; _++_)

  open import Data.String renaming (_==_ to _≛_ ; _++_ to _⊍_; show to showString) -- U+225B U+228D
  open import Data.Char renaming (_==_ to _≐_ ; show to toString) -- U+2250
  open import Data.Bool using (true ; false)

  coSplit′ : Costring → Costring
  coSplit′ [] = []
  coSplit′ (x ∷ xs) with x ≐ '!'
  ... | false = x ∷ ♯ coSplit′ (♭ xs)
  ... | true = '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs))

  coSplit″ : Costring → Costring
  coSplit″ [] = []
  coSplit″ (x ∷ xs) with x ≐ '!'
  ... | false = x ∷ ♯ coSplit″ (♭ xs)
  ... | true = (toCostring ">>") ++ coSplit″ (♭ xs)

  main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘ coSplit′) s
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180730/1751f5f4/attachment.sig>