<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 NO_TERMINATION_CHECK allowed you to say "I promise this is terminating, so please treat it as such and unfold it during type checking". Is there no way to turn off the termination checker in such a way that things reduce any more? </div><div><div><br></div><div>-Dan</div><div><br><div><div>On Jul 4, 2014, at 5:45 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> 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"><<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>
_______________________________________________<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>