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

[Andreas Abel]

Yes, the error location is wrong when clause tri> comes before 
tri\approx (otherwise it is correct).  Weird.

On 11.02.2015 14:18, Andrés Sicard-Ramírez wrote:
>
> On 11 February 2015 at 05:37, Sergei Meshveliani <mechvel at botik.ru
> <mailto: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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/