add interface for compatibility between Eq and Ord

leesongun

Mar 9, 2023, 6:08 PM

YIWX5KUGM4NC2NCS5IZSAIUGYAVNOR4ARF5KVZHS3QRLLWLO6VKQC

Dependencies

• [2] VCJVFB63 add total ordering

Change contents

• file addition: EqOrd.idr (----------)
  [2.19]
  + module Control.EqOrd

  +

  + --Eq and Ord compatibility

  + public export

  + interface Ord ty => EqOrd ty where

  + eqord : (x, y : ty) -> (x == y) = (compare x y == EQ)

  +

  + export

  + EqOrd Nat where

  + eqord 0 0 = Refl

  + eqord 0 (S _) = Refl

  + eqord (S _) 0 = Refl

  + eqord (S i) (S j) = eqord i j