[Agda] question on `compare'

[Peter Selinger]

I think the problem is ≤refl m=n. It should be ≤refl n=m instead.
-- Peter

Sergei Meshveliani 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
>     }
> ---------------------------------------------------------------
> 
> " n != m of type ℕ
>   when checking that the expression n≤m has type m ≤ n
> "
> 
> The signature for ≮→≥  ends with  m ≤ n. 
> 
> So, why does  Agda 2.4.2.2  expect  m ≤ n
> ?
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>