0 | ||| Additional data types related to ordering notions
 1 | module Data.Order
 2 |
 3 | %default total
 4 |
 5 | ||| Trichotomous formalises the fact that three relations are mutually exclusive.
 6 | ||| It is meant to be used with relations that complement each other so that the
 7 | ||| `Trichotomous lt eq gt` relation is the total relation.
 8 | public export
 9 | data Trichotomous : (lt, eq, gt : a -> a -> Type) -> (a -> a -> Type) where
10 |   MkLT : {0 lt, eq, gt : a -> a -> Type} ->
11 |          lt v w       -> Not (eq v w) -> Not (gt v w) -> Trichotomous lt eq gt v w
12 |   MkEQ : {0 lt, eq, gt : a -> a -> Type} ->
13 |          Not (lt v w) -> eq v w       -> Not (gt v w) -> Trichotomous lt eq gt v w
14 |   MkGT : {0 lt, eq, gt : a -> a -> Type} ->
15 |          Not (lt v w) -> Not (eq v w) -> gt v w       -> Trichotomous lt eq gt v w
16 |