[Agda] termination by contradiction

[Ulf Norell]

On Wed, Jul 2, 2014 at 7:42 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> 2) Suppose one introduces `loopy' by a mistake, and sets its various
> invocations, also by a mistake. What can happen then, in the worst case?
> Probably, the type checker will loop forever, and the user will
> interrupt the process of checking (as I did 10 minutes ago!).
> This will not make the whole usage worse, because there are many other
> ways in Agda to make the checker loop forever.
>

There shouldn't be any ways to make the type checker loop forever, so if
you have
any, please report them as bugs. There's a big difference between the type
checker
looping and there being inefficiencies in the type checker or your program,
making
checking take a very long time (or run out of memory).

 / Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140702/b77b5748/attachment.html