[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