[Agda] Codata error
Sergei Meshveliani
mechvel at botik.ru
Wed Jan 2 13:47:22 CET 2019
On Wed, 2019-01-02 at 13:15 +0100, Nils Anders Danielsson wrote:
> On 30/12/2018 18.10, Sergei Meshveliani wrote:
> > 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.
>
> If you use the experimental branch of the standard library, and the
> master branch of Agda, then your code is accepted.
>
The www page shows the git command for Development version.
But it occurs that the experimental branch is inside it
(I have got it with the hint given by Guillaume).
May be the page needs to add an instruction for getting the experimental
branch.
Regards,
------
Sergei
More information about the Agda
mailing list