[Agda] question on `compare'

[Sergei Meshveliani]

Indeed! Thank you.

------
Sergei



On Wed, 2015-02-11 at 08:43 -0400, Peter Selinger wrote:
> 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
> > 
> 
>