Add various instances from stdlib interfaces (Eq, Ord, DecEq)

For Void and Either

This is because I ended up using them elsewhere, so why not include them in the stdlib.

Also expose left/rightInjective functions, as are used in the DecEq proofs.

libs/base/Data/Either.idr

@@ -65,9 +65,11 @@ eitherToMaybe (Right x) = Just x
 -- Injectivity of constructors
 
 ||| Left is injective
+export
 leftInjective : Left x = Left y -> x = y
 leftInjective Refl = Refl
 
 ||| Right is injective
+export
 rightInjective : Right x = Right y -> x = y
 rightInjective Refl = Refl

libs/base/Decidable/Equality.idr

@@ -1,6 +1,7 @@
 module Decidable.Equality
 
 import Data.Maybe
+import Data.Either
 import Data.Nat
 import Data.List
 
@@ -78,6 +79,27 @@ DecEq t => DecEq (Maybe t) where
     decEq (Just x') (Just y') | No p
        = No $ \h : Just x' = Just y' => p $ justInjective h
 
+--------------------------------------------------------------------------------
+-- Either
+--------------------------------------------------------------------------------
+
+Uninhabited (Left x = Right y) where
+  uninhabited Refl impossible
+
+Uninhabited (Right x = Left y) where
+  uninhabited Refl impossible
+
+export
+(DecEq t, DecEq s) => DecEq (Either t s) where
+  decEq (Left x) (Left y) with (decEq x y)
+   decEq (Left x) (Left x) | Yes Refl = Yes Refl
+   decEq (Left x) (Left y) | No contra = No (contra . leftInjective)
+  decEq (Left x) (Right y) = No absurd
+  decEq (Right x) (Left y) = No absurd
+  decEq (Right x) (Right y) with (decEq x y)
+   decEq (Right x) (Right x) | Yes Refl = Yes Refl
+   decEq (Right x) (Right y) | No contra = No (contra . rightInjective)
+
 --------------------------------------------------------------------------------
 -- Tuple
 --------------------------------------------------------------------------------

libs/prelude/Prelude/EqOrd.idr

@@ -19,6 +19,10 @@ interface Eq ty where
   x == y = not (x /= y)
   x /= y = not (x == y)
 
+public export
+Eq Void where
+  _ == _ impossible
+
 public export
 Eq () where
   _ == _ = True
@@ -102,6 +106,10 @@ interface Eq ty => Ord ty where
   min : ty -> ty -> ty
   min x y = if (x < y) then x else y
 
+public export
+Ord Void where
+  compare _ _ impossible
+
 public export
 Ord () where
   compare _ _ = EQ