[Agda] termination by contradiction

[Sergei Meshveliani]

On Wed, 2014-07-02 at 22:55 +0200, Ulf Norell wrote:
> 
> 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).
> 


I see. Thank you.

As to Markov's rule for termination, I understand this as follows.
1) It can be used in an Agda program by postulating termination like it
is done in  NO_TERMINATION_CHECK for  findNatByContra.
2) This will lead to a  non-terminated  type-check for some functions 
applying  findNatByContra  
(and I doubt on whether such functions can appear in a practical program
other than by a mistake).

Regards,

------
Sergei