[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