<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 11 February 2015 at 05:37, 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: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 (ℕ; _≮_; _≤_; _≥_; _<_)<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 <→≤ : ∀ {m n} → m < 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< m<n _ _ ) → ⊥-elim (m≮n m<n)<br>
; (tri≈ _ m=n _ ) → ≤refl m=n<br>
; (tri> _ _ m>n) → let n<m : n < m<br>
n<m = m>n<br>
<br>
n≤m : n ≤ m<br>
n≤m = <→≤ {n} {m} n<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< m<n _ _ = ⊥-elim (m≮n m<n)<br>≮→≥ m≮n | tri≈ _ m=n _ = ≤refl m=n<br>≮→≥ {m} {n} m≮n | tri> _ _ m>n =<br> let n<m : n < m<br> n<m = m>n<br><br> n≤m : n ≤ m<br> n≤m = <→≤ {n} {m} n<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>