<div dir="ltr">I'm not sure what the different behaviour you are getting is (can you elaborate?), but f can be implemented as follows:<div><br></div><div><div>⊥-elim-irr : .⊥ → ∀ {a} {A : Set a} → A</div><div>⊥-elim-irr ()</div>
<div><br></div><div><span style="font-family:arial,sans-serif;font-size:13px">f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0</span><br></div><div>f x nz z = ⊥-elim-irr (nz z)</div></div><div><br></div><div>Under normal circumstances irrelevant things cannot be used in relevant contexts, but one exception is that you are allowed absurd elimination of irrelevant empty types into relevant types.</div>
<div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Aug 20, 2014 at 1:49 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">Dear Agda developers,<br>
<br>
Agda of August 19 2014 type-checks irrelevant arguments in a different<br>
way than Agda-2.4.0.2.<br>
So that some of my code is not type-checked any more.<br>
I have the two questions on the subject.<br>
<br>
1. Which treating is more correct?<br>
<br>
2. For example, how to implement the function<br>
<br>
f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0<br>
f x ???<br>
<br>
?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
</blockquote></div><br></div>