[Agda] Termination checker change?

[Catarina Coquand]

Hi,


I changed that recently to be able to deal with hidden arguments. The 
problem
when checking termination for definitions with hidden arguments is that one
needs to type check in order to put back the hidden information.  So the 
complaint
is because Agda re-typechecks and then it will complain because the 
definitions are
allready type-checked. Maybe you can just ignore the error for now? 
Should one
have an option indicating if they  contains hidden arguments, or not?

In fact this is a problem for emacs-agda also.


Regards

       Catarina


Thomas Hallgren wrote:

> Hi,
>
> Has there been a change in how to call the termination checker in 
> Agda? When I try to use it from Alfa, all I get is errors about 
> duplicate definitions...
>
>------------------------------------------------------------------------
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>http://lists.chalmers.se/mailman/listinfo/agda
>  
>