<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 11 February 2015 at 05:37, 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":1kq" class="" style="overflow:hidden">Please, what is wrong here?<br>
<br>
--------------------------------------------------------------------<br>
open import Function        using (case_of_)<br>
open import Relation.Binary using (module DecTotalOrder;<br>
                                   module StrictTotalOrder; module Tri)<br>
open import Data.Empty using (⊥-elim)<br>
open import Data.Nat as Nat using (ℕ; _≮_; _≤_; _≥_; _&lt;_)<br>
open import Data.Nat.Properties as NatProp using ()<br>
<br>
open StrictTotalOrder NatProp.strictTotalOrder using (compare)<br>
open DecTotalOrder    Nat.decTotalOrder using ()<br>
                                        renaming (reflexive to ≤refl)<br>
open Tri<br>
<br>
<br>
postulate  &lt;→≤ : ∀ {m n} → m &lt; n → m ≤ n<br>
<br>
≮→≥ : ∀ {m n} → m ≮ n → n ≤ m<br>
≮→≥ {m} {n} m≮n =<br>
    case compare m n<br>
    of \<br>
    { (tri&lt; m&lt;n _   _   ) → ⊥-elim (m≮n m&lt;n)<br>
    ; (tri≈ _   m=n _   ) → ≤refl m=n<br>
    ; (tri&gt; _   _    m&gt;n) → let n&lt;m : n &lt; m<br>
                                n&lt;m = m&gt;n<br>
<br>
                                n≤m : n ≤ m<br>
                                n≤m = &lt;→≤ {n} {m} n&lt;m<br>
                            in<br>
                            n≤m<br>
    }</div></blockquote></div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">​Rewriting the function by<br><br>≮→≥ : ∀ {m n} → m ≮ n → n ≤ m<br>≮→≥ {m} {n} m≮n with compare m n<br>≮→≥         m≮n | tri&lt; m&lt;n _   _   = ⊥-elim (m≮n m&lt;n)<br>≮→≥         m≮n | tri≈ _   m=n _   = ≤refl m=n<br>≮→≥ {m} {n} m≮n | tri&gt; _   _   m&gt;n =<br>  let n&lt;m : n &lt; m<br>      n&lt;m = m&gt;n<br><br>      n≤m : n ≤ m<br>      n≤m = &lt;→≤ {n} {m} n&lt;m<br>  in n≤m<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Why does ​Agda (correctly) report the error ​in `≤refl m=n`, but using the original function Agda reports the error `n≤m`?<br></div><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">Andrés</div></div></div></div>
</div></div>