[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