<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
> Using NO_TERMINATION_CHECK is not going to cause the type<br>
> checker to loop. What happens is that the type checker simply won't<br>
> 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 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 "done")<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's a bug, which I'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>