
  0 | ||| Provides a type for proving compatibility between Eq and Ord
  1 | module Decidable.EqOrd
  2 | 
  3 | 
  4 | ||| Compatibility between Eq and Ord
  5 | public export
  6 | data EqOrdCompat : Bool -> Ordering -> Type where
  7 |   LT : EqOrdCompat False LT
  8 |   GT : EqOrdCompat False GT
  9 |   EQ : EqOrdCompat True EQ
 10 | 
 11 | 
 12 | ||| Types with compatible Eq and Ord instances
 13 | public export
 14 | interface Ord x => OrdCompatible x where
 15 |   eqOrdCompat : (a : x) -> (b : x) -> EqOrdCompat (a == b) (compare a b)
 16 | 
 17 | public export
 18 | OrdCompatible () where
 19 |   eqOrdCompat () () = EQ
 20 | 
 21 | public export
 22 | OrdCompatible Bool where
 23 |   eqOrdCompat True True = EQ
 24 |   eqOrdCompat False False = EQ
 25 |   eqOrdCompat True False = GT
 26 |   eqOrdCompat False True = LT
 27 | 
 28 | public export
 29 | eqOrdCompatSucc : EqOrdCompat (a == b) (compare a b) -> EqOrdCompat (S a == S b) (compare (S a) (S b))
 30 | eqOrdCompatSucc {a} {b} c with 0 (a == b) | 0 (compare a b)
 31 |   eqOrdCompatSucc EQ | True | EQ = EQ
 32 |   eqOrdCompatSucc GT | False | GT = GT
 33 |   eqOrdCompatSucc LT | False | LT = LT
 34 | 
 35 | public export
 36 | OrdCompatible Nat where
 37 |   eqOrdCompat 0 0 = EQ
 38 |   eqOrdCompat (S m) 0 = GT
 39 |   eqOrdCompat 0 (S n) = LT
 40 |   eqOrdCompat (S m) (S n) = eqOrdCompatSucc (eqOrdCompat m n)
 41 |