+ module Control.Total
+
+ -- Antisymmetricity (Reflexivity also follows)
+ public export
+ interface Ord ty => AntiSym ty where
+ antisym : (x,y:ty) -> (compare x y) = contra (compare y x)
+
+ export
+ possibles : Ordering -> Ordering -> Type
+ possibles LT GT = Void
+ possibles GT LT = Void
+ possibles _ _ = ()
+
+ -- Transitivity
+ public export
+ interface Ord ty => Trans ty where
+ trans : (x,y,z:ty) -> {auto p: possibles (compare x y) (compare y z)} -> compare x y <+> compare y z = compare x z
+
+ public export
+ interface (AntiSym ty, Trans ty) => Total ty where
+
+ export
+ AntiSym Nat where
+ antisym 0 0 = Refl
+ antisym 0 (S k) = Refl
+ antisym (S k) 0 = Refl
+ antisym (S k) (S j) = antisym k j
+
+ export
+ Trans Nat where
+ trans 0 0 0 = Refl
+ trans 0 0 (S _) = Refl
+ trans 0 (S _) (S _) = Refl
+ trans (S _) 0 0 = Refl
+ trans (S i) (S j) 0 with (compare i j)
+ _ | EQ = Refl
+ _ | GT = Refl
+ trans (S i) (S j) (S k) = trans i j k
+
+ export
+ Total Nat where