[Agda] Wrong reporting error ? (Was question on `compare')

[Andrés Sicard-Ramírez]

On 11 February 2015 at 05:37, Sergei Meshveliani <mechvel at botik.ru> wrote:

> Please, what is wrong here?
>
> --------------------------------------------------------------------
> open import Function        using (case_of_)
> open import Relation.Binary using (module DecTotalOrder;
>                                    module StrictTotalOrder; module Tri)
> open import Data.Empty using (⊥-elim)
> open import Data.Nat as Nat using (ℕ; _≮_; _≤_; _≥_; _<_)
> open import Data.Nat.Properties as NatProp using ()
>
> open StrictTotalOrder NatProp.strictTotalOrder using (compare)
> open DecTotalOrder    Nat.decTotalOrder using ()
>                                         renaming (reflexive to ≤refl)
> open Tri
>
>
> postulate  <→≤ : ∀ {m n} → m < n → m ≤ n
>
> ≮→≥ : ∀ {m n} → m ≮ n → n ≤ m
> ≮→≥ {m} {n} m≮n =
>     case compare m n
>     of \
>     { (tri< m<n _   _   ) → ⊥-elim (m≮n m<n)
>     ; (tri≈ _   m=n _   ) → ≤refl m=n
>     ; (tri> _   _    m>n) → let n<m : n < m
>                                 n<m = m>n
>
>                                 n≤m : n ≤ m
>                                 n≤m = <→≤ {n} {m} n<m
>                             in
>                             n≤m
>     }
>

​Rewriting the function by

≮→≥ : ∀ {m n} → m ≮ n → n ≤ m
≮→≥ {m} {n} m≮n with compare m n
≮→≥         m≮n | tri< m<n _   _   = ⊥-elim (m≮n m<n)
≮→≥         m≮n | tri≈ _   m=n _   = ≤refl m=n
≮→≥ {m} {n} m≮n | tri> _   _   m>n =
  let n<m : n < m
      n<m = m>n

      n≤m : n ≤ m
      n≤m = <→≤ {n} {m} n<m
  in n≤m

Why does ​Agda (correctly) report the error ​in `≤refl m=n`, but using the
original function Agda reports the error `n≤m`?

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150211/6d994e7e/attachment.html