1 files changed, 17 insertions, 1 deletions
diff --git a/src/CHAD/Data.hs b/src/CHAD/Data.hs
index 8c7605c..68b2554 100644
--- a/src/CHAD/Data.hs
+++ b/src/CHAD/Data.hs
@@ -8,11 +8,13 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-module CHAD.Data (module CHAD.Data, (:~:)(Refl), If) where
+module CHAD.Data (module CHAD.Data, (:~:)(Refl), If, EqP(eqp), OrdP(comparep)) where
 
+import Data.EqP
 import Data.Functor.Product
 import Data.GADT.Compare
 import Data.GADT.Show
+import Data.OrdP
 import Data.Some
 import Data.Type.Bool (If)
 import Data.Type.Equality
@@ -86,6 +88,11 @@ instance TestEquality SNat where testEquality = geq
 instance GEq SNat where geq = defaultGeq
 instance GShow SNat where gshowsPrec = defaultGshowsPrec
 
+instance Eq (SNat n) where _ == _ = True
+instance Ord (SNat n) where compare _ _ = EQ
+instance EqP SNat where eqp = eqpFromGEq
+instance OrdP SNat where comparep = comparepFromGCompare
+
 fromSNat :: SNat n -> Int
 fromSNat SZ = 0
 fromSNat (SS n) = succ (fromSNat n)
@@ -190,3 +197,12 @@ data SBool b where
   SF :: SBool False
   ST :: SBool True
 deriving instance Show (SBool b)
+
+eqpFromGEq :: GEq f => f a -> f b -> Bool
+eqpFromGEq x y = case geq x y of
+                   Just Refl -> True
+                   Nothing -> False
+
+comparepFromGCompare :: GCompare f => f a -> f b -> Ordering
+comparepFromGCompare x y = case gcompare x y of
+                             GEQ -> EQ ; GLT -> LT ; GGT -> GT