Data.Type.Witness.General.Order

Documentation

data WOrdering (a :: k) (b :: k) where

Constructors

WLT :: forall k (a :: k) (b :: k). WOrdering a b

WEQ :: forall k (a :: k). WOrdering a a

WGT :: forall k (a :: k) (b :: k). WOrdering a b

wOrderingToOrdering :: WOrdering a b -> Ordering

class TestEquality w => TestOrder (w :: k -> Type) where

Methods

testCompare :: forall (a :: k) (b :: k). w a -> w b -> WOrdering a b

Instances

TestOrder NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

testCompare :: forall (a :: k) (b :: k). NaturalType a -> NaturalType b -> WOrdering a b

TestOrder PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

testCompare :: forall (a :: k) (b :: k). PeanoNatType a -> PeanoNatType b -> WOrdering a b

TestOrder SymbolType

Defined in Data.Type.Witness.Specific.Symbol

Methods

testCompare :: forall (a :: k) (b :: k). SymbolType a -> SymbolType b -> WOrdering a b

TestOrder (EmptyType :: k -> Type)

Defined in Data.Type.Witness.Specific.Empty

Methods

testCompare :: forall (a :: k0) (b :: k0). EmptyType a -> EmptyType b -> WOrdering a b

TestOrder (ListElementType tt :: k -> Type)

Defined in Data.Type.Witness.Specific.List.Element

Methods

testCompare :: forall (a :: k0) (b :: k0). ListElementType tt a -> ListElementType tt b -> WOrdering a b

TestOrder w1 => TestOrder (PairType w1 w2 :: k -> Type)

left-biased

Defined in Data.Type.Witness.Specific.Pair

Methods

testCompare :: forall (a :: k0) (b :: k0). PairType w1 w2 a -> PairType w1 w2 b -> WOrdering a b