<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Wait, I'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&nbsp;NO_TERMINATION_CHECK allowed you to say "I promise this is terminating, so please treat it as such and unfold it during type checking". &nbsp;Is there no way to turn off the termination checker in such a way that things reduce any more? &nbsp;</div><div><div><br></div><div>-Dan</div><div><br><div><div>On Jul 4, 2014, at 5:45 AM, Ulf Norell &lt;<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>&gt; wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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 class="">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't<br>
&gt; evaluate functions that haven'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 &nbsp; &nbsp; &nbsp; &nbsp; using (case_of_)<br>
open import Relation.Nullary using (yes; no; ¬_)<br>
open import Relation.Unary &nbsp; using (Decidable)<br>
open import Relation.Binary.PropositionalEquality as PE using<br>
&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;(_≡_; refl)<br>
open import Data.Empty &nbsp; using (⊥)<br>
open import Data.Product using (_,_; proj₁; Σ)<br>
open import Data.Nat &nbsp; &nbsp; using (ℕ; suc)<br>
<br>
{-# NO_TERMINATION_CHECK #-}<br>
<div class="">findNatByContra :<br>
&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
findNatByContra P P? _ = &nbsp;findFrom 0<br>
&nbsp; where<br>
&nbsp; findFrom : ℕ → Σ ℕ P<br>
&nbsp; findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; ; (no _) &nbsp; → findFrom (suc n) }<br>
</div><div class="">False : ℕ → Set<br>
False _ = ⊥<br>
<br>
decFalse : Decidable False<br>
decFalse _ = no (λ x → x)<br>
<br>
loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
loopy H = &nbsp;findNatByContra False decFalse H<br>
<br>
</div><div class="">thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42<br>
thm _ = refl<br>
<br>
</div>main : IO Unit<br>
main = putStrLn (toCostring "done")<br>
----------------------------------------------------------------------<br>
<br>
1) The checker loops at it &nbsp;(Agda 2.4.0).<br>
2) If &nbsp;thm &nbsp;is removed, than it is checked and compiled.<br></blockquote><div><br></div><div>That's a bug, which I've now fixed.</div><div>&nbsp;</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>
&nbsp; &nbsp;function &nbsp;findNatByContra. &nbsp;Right?<br></blockquote><div>&nbsp;</div><div>Yes.</div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></div></div></body></html>