[Agda] Codata error

Sergei Meshveliani mechvel at botik.ru
Sun Dec 30 11:57:48 CET 2018


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




More information about the Agda mailing list