<div dir="ltr">I think the name fits quite well with the usual meaning of non-termination. You just have to keep in mind that we care not only about run-time termination, but also compile-time termination on open terms. In your case findNatByContra is non-terminating in the presence of false assumptions. If you have a function that is really terminating on closed as well as open terms, then NO_TERMINATION_CHECK will work just fine.<div>

<br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jul 7, 2014 at 8:15 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">On Mon, 2014-07-07 at 21:56 +0400, Sergei Meshveliani wrote:<br>
&gt; On Mon, 2014-07-07 at 18:11 +0200, Ulf Norell wrote:<br>
&gt; &gt;<br>
&gt; &gt; On Mon, Jul 7, 2014 at 2:36 PM, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt;<br>
&gt; &gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt;         I have installed Agda of July 7, 2014<br>
&gt; &gt;         (in which the checker loop is fixed), and tried this program<br>
&gt; &gt;         version:<br>
&gt; &gt;         ----------------------------------------------------------------<br>
&gt; &gt;         {-# NO_TERMINATION_CHECK #-}<br>
&gt; &gt;         findNatByContra :<br>
&gt; &gt;                (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
&gt; &gt;         findNatByContra P P? _ =  find>From 0<br>
&gt; &gt;           where<br>
&gt; &gt;           findFrom : ℕ → Σ ℕ P<br>
&gt; &gt;           findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
&gt; &gt;                                       ; (no _)   → findFrom (suc n) }<br>
</div>&gt; &gt; [..]<br>
<div class="">&gt;<br>
&gt; &gt;         I am trying to provide the feature ``classic termination<br>
&gt; &gt;         proof&#39;&#39; with<br>
&gt; &gt;         some possibilities in Agda.<br>
</div>&gt; &gt; [..]<br>
<div class=""><br>
<br>
&gt; First of all, I got overruled on the behaviour of<br>
&gt; NO_TERMINATION_CHECK. I&#39;ve implemented a new pragma NON_TERMINATING<br>
&gt; with the non-looping behaviour.<br>
<br>
</div>1) As I wrote before, the word  `non-terminating&#39;  (algorithm Foo)<br>
<div class="">   already has a default meaning:<br>
   ``Foo does not terminate at each argument&#39;&#39;,<br>
   or may be,  ``Foo does not terminate at some argument&#39;&#39;.<br>
<br>
</div>2) Is the word  TERMINATES  adequate?<br>
   (the meaning is ``postulate that it terminates&#39;&#39;).<br>
<br>
Regards,<br>
<div class="HOEnZb"><div class="h5"><br>
------<br>
Sergei<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>