<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&#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 class="">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 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 =  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 &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>