[Agda] Codata error

Caryo Scelus caryoscelus at gmx.com
Sun Dec 30 13:02:57 CET 2018


On Sun, 30 Dec 2018 13:57:48 +0300
Sergei Meshveliani <mechvel at botik.ru> wrote:

> Can anybody, please, tell how to fix the following program?
> 
> --------------------------------------
> open import Foreign.Haskell
> open import IO.Primitive
> open import Codata.Musical.Costring using (toCostring)
> 
> main : IO Unit
> main = putStrLn (toCostring "abc")
> --------------------------------------
> 
> Development Agda of December 23, 2018
> reports of
>         Termination check failure in  Codata.Musical.Conat.
> 
> Is this a bug in Agda? 
> Do I misuse the Development Standard library of December 23, 2018 ?
> 
> Thanks,
> 
> ------
> Sergei

I don't know what exactly is going on, but a solution that works for me
is to use `experimental` branch of stdlib.


More information about the Agda mailing list