<div dir="ltr">The --no-termination-check flag will still treat functions as terminating. The motivation for the<br><div>new behaviour (which I honestly thought was the intended behaviour all along) is to let you</div><div>

write possibly non-terminating programs without jeopardising decidability of type checking.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 4, 2014 at 3:45 PM, Dan Licata <span dir="ltr">&lt;<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Wait, I&#39;m confused.<div><br></div><div>I thought from the comment that<div><br></div>

<pre style="margin-top:0px;margin-bottom:0px;padding:1em;line-height:1.1em;clear:both;background-color:rgb(249,249,249)">Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
    Agda treat any function as terminating.</pre><div><br></div><div>in the 2.4.0 release notes that NO_TERMINATION_CHECK allowed you to say &quot;I promise this is terminating, so please treat it as such and unfold it during type checking&quot;.  Is there no way to turn off the termination checker in such a way that things reduce any more?  </div>

<div><span class="HOEnZb"><font color="#888888"><div><br></div><div>-Dan</div></font></span><div><br><div><div><div class="h5"><div>On Jul 4, 2014, at 5:45 AM, Ulf Norell &lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt; wrote:</div>

<br></div></div><blockquote type="cite"><div><div class="h5"><div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jul 3, 2014 at 6: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>On Thu, 2014-07-03 at 15:06 +0200, Ulf Norell wrote:<br>
&gt; Using NO_TERMINATION_CHECK is not going to cause the type<br>
&gt; checker to loop. What happens is that the type checker simply won&#39;t<br>
&gt; evaluate functions that haven&#39;t been termination checked.<br>
<br>
<br>
</div>How does the below program correspond to these your two assertions?<br>
<br>
----------------------------------------------------------------------<br>
open import Foreign.Haskell<br>
open import IO.Primitive<br>
open import Data.String as String using (toCostring)<br>
open import Function         using (case_of_)<br>
open import Relation.Nullary using (yes; no; ¬_)<br>
open import Relation.Unary   using (Decidable)<br>
open import Relation.Binary.PropositionalEquality as PE using<br>
                                                     (_≡_; refl)<br>
open import Data.Empty   using (⊥)<br>
open import Data.Product using (_,_; proj₁; Σ)<br>
open import Data.Nat     using (ℕ; suc)<br>
<br>
{-# NO_TERMINATION_CHECK #-}<br>
<div>findNatByContra :<br>
            (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
findNatByContra P P? _ =  findFrom 0<br>
  where<br>
  findFrom : ℕ → Σ ℕ P<br>
  findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
                              ; (no _)   → findFrom (suc n) }<br>
</div><div>False : ℕ → Set<br>
False _ = ⊥<br>
<br>
decFalse : Decidable False<br>
decFalse _ = no (λ x → x)<br>
<br>
loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
loopy H =  findNatByContra False decFalse H<br>
<br>
</div><div>thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42<br>
thm _ = refl<br>
<br>
</div>main : IO Unit<br>
main = putStrLn (toCostring &quot;done&quot;)<br>
----------------------------------------------------------------------<br>
<br>
1) The checker loops at it  (Agda 2.4.0).<br>
2) If  thm  is removed, than it is checked and compiled.<br></blockquote><div><br></div><div>That&#39;s a bug, which I&#39;ve now fixed.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">




3) In expect that this NO_TERMINATION_CHECK applies only to the<br>
   function  findNatByContra.  Right?<br></blockquote><div> </div><div>Yes.</div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div></div></div><div class="">
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">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></blockquote></div><br></div></div></div></div></blockquote></div><br></div>