[Agda] termination by contradiction

[Sergei Meshveliani]

On Mon, 2014-07-07 at 21:56 +0400, Sergei Meshveliani wrote:
> On Mon, 2014-07-07 at 18:11 +0200, Ulf Norell wrote:
> > 
> > On Mon, Jul 7, 2014 at 2:36 PM, Sergei Meshveliani <mechvel at botik.ru>
> > wrote:        
> >         
> >         I have installed Agda of July 7, 2014
> >         (in which the checker loop is fixed), and tried this program
> >         version:  
> >         ----------------------------------------------------------------
> >         {-# NO_TERMINATION_CHECK #-}
> >         findNatByContra :
> >                (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P
> >         findNatByContra P P? _ =  findFrom 0
> >           where
> >           findFrom : ℕ → Σ ℕ P
> >           findFrom n = case P? n of \ { (yes Pn) → (n , Pn)
> >                                       ; (no _)   → findFrom (suc n) }
> > [..]
>      
> >         I am trying to provide the feature ``classic termination
> >         proof'' with
> >         some possibilities in Agda.
> > [..] 


> First of all, I got overruled on the behaviour of
> NO_TERMINATION_CHECK. I've implemented a new pragma NON_TERMINATING
> with the non-looping behaviour.

1) As I wrote before, the word  `non-terminating'  (algorithm Foo)  
   already has a default meaning:
   ``Foo does not terminate at each argument'', 
   or may be,  ``Foo does not terminate at some argument''.

2) Is the word  TERMINATES  adequate?
   (the meaning is ``postulate that it terminates'').

Regards,

------
Sergei