[Agda] Codata error

Sergei Meshveliani mechvel at botik.ru
Sun Dec 30 18:10:27 CET 2018


On Sun, 2018-12-30 at 12:02 +0000, Caryo Scelus wrote:
> 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.


Now I tried Experimental branches of Agda and of stdlib both of 
December 30, 2018.
And it yields   Termination check failure in  Codata.Musical.Conat.

May be this error is only in a fresh enough version ...

--
SM



More information about the Agda mailing list