[Agda] Checking termination is not sufficiently exploratory.

[a.j.rouvoet]

For coSplit to pass the checker, the recursive invocation must appear 
guarded by a constructor.
This is clearly the case in coSplit', but not necessarily in coSplit'' 
(e.g. when toString ">>" returns the empty costring).


On 07/30/2018 04:55 PM, Serge Leblanc wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180730/94a3c3de/attachment.html>