[Agda] Termination checker change?

Andreas Abel abel at cs.chalmers.se
Thu Nov 4 11:09:22 MET 2004


Hi Thomas,

Catarina told me the termination checker is broken in the current 
version since she has not updated it to implicit arguments and type classes.

The problem with duplicate definitions could be something else, since 
these errors arise also when you have conflicts with the Agda prelude, 
like defining another List type.  I am just wildly guessing here.

Catarina told me she is away for the rest of the week.

Andreas

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...

-- 
Andreas Abel  <><      --<>--    Du bist der geliebte Mensch.

Dept. of Computer Science,  Chalmers University of Technology
Rännvägen 6, rum 5119, 41296 Göteborg, SWEDEN, +46-31-7721006


More information about the Agda mailing list