Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Ord

Contents

Defunctionalization symbols

Description

Defines the promoted version of Ord, POrd, and the singleton version, SOrd.

Synopsis

class PEq a => POrd (a :: Type) where
- type Compare (arg :: a) (arg :: a) :: Ordering
- type (arg :: a) < (arg :: a) :: Bool
- type (arg :: a) <= (arg :: a) :: Bool
- type (arg :: a) > (arg :: a) :: Bool
- type (arg :: a) >= (arg :: a) :: Bool
- type Max (arg :: a) (arg :: a) :: a
- type Min (arg :: a) (arg :: a) :: a
class SEq a => SOrd a where
type family Comparing (a :: TyFun b a -> Type) (a :: b) (a :: b) :: Ordering where ...
sComparing :: forall (t :: TyFun b a -> Type) (t :: b) (t :: b). SOrd a => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ComparingSym0 t) t) t :: Ordering)
thenCmp :: Ordering -> Ordering -> Ordering
type family ThenCmp (a :: Ordering) (a :: Ordering) :: Ordering where ...
sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering)
data family Sing (a :: k)
data ThenCmpSym0 (l :: TyFun Ordering (TyFun Ordering Ordering -> Type))
data ThenCmpSym1 (l :: Ordering) (l :: TyFun Ordering Ordering)
type ThenCmpSym2 (t :: Ordering) (t :: Ordering) = ThenCmp t t
type LTSym0 = LT
type EQSym0 = EQ
type GTSym0 = GT
data CompareSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Ordering -> Type))
data CompareSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 Ordering)
type CompareSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Compare t t
data (<@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type))
data (l :: a6989586621679315171) <@#@$$ (l :: TyFun a6989586621679315171 Bool)
type (<@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (<) t t
data (<=@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type))
data (l :: a6989586621679315171) <=@#@$$ (l :: TyFun a6989586621679315171 Bool)
type (<=@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (<=) t t
data (>@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type))
data (l :: a6989586621679315171) >@#@$$ (l :: TyFun a6989586621679315171 Bool)
type (>@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (>) t t
data (>=@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type))
data (l :: a6989586621679315171) >=@#@$$ (l :: TyFun a6989586621679315171 Bool)
type (>=@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (>=) t t
data MaxSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type))
data MaxSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 a6989586621679315171)
type MaxSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Max t t
data MinSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type))
data MinSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 a6989586621679315171)
type MinSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Min t t
data ComparingSym0 (l :: TyFun (TyFun b6989586621679315161 a6989586621679315160 -> Type) (TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> Type))
data ComparingSym1 (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (l :: TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type))
data ComparingSym2 (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (l :: b6989586621679315161) (l :: TyFun b6989586621679315161 Ordering)
type ComparingSym3 (t :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (t :: b6989586621679315161) (t :: b6989586621679315161) = Comparing t t t

Documentation

class PEq a => POrd (a :: Type) #

Associated Types

type Compare (arg :: a) (arg :: a) :: Ordering #

type (arg :: a) < (arg :: a) :: Bool #

type (arg :: a) <= (arg :: a) :: Bool #

type (arg :: a) > (arg :: a) :: Bool #

type (arg :: a) >= (arg :: a) :: Bool #

type Max (arg :: a) (arg :: a) :: a #

type Min (arg :: a) (arg :: a) :: a #

Instances

POrd Bool #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd Ordering #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd Nat #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd Symbol #
Instance details Defined in Data.Singletons.TypeLits.Internal Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd () #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd Void #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd [a] #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (Maybe a) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (NonEmpty a) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (Either a b) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b, c) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b, c, d) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b, c, d, e) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b, c, d, e, f) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
POrd (a, b, c, d, e, f, g) #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #

class SEq a => SOrd a where #

Methods

sCompare :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) #

(%<) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) infix 4 #

(%<=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) infix 4 #

(%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) infix 4 #

(%>=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) infix 4 #

sMax :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) #

sMin :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) #

sCompare :: forall (t :: a) (t :: a). ((Apply (Apply CompareSym0 t) t :: Ordering) ~ Apply (Apply Compare_6989586621679316629Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t :: Ordering) #

(%<) :: forall (t :: a) (t :: a). ((Apply (Apply (<@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679316662Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) infix 4 #

(%<=) :: forall (t :: a) (t :: a). ((Apply (Apply (<=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679316695Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) infix 4 #

(%>) :: forall (t :: a) (t :: a). ((Apply (Apply (>@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679316728Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) infix 4 #

(%>=) :: forall (t :: a) (t :: a). ((Apply (Apply (>=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679316761Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) infix 4 #

sMax :: forall (t :: a) (t :: a). ((Apply (Apply MaxSym0 t) t :: a) ~ Apply (Apply Max_6989586621679316794Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t :: a) #

sMin :: forall (t :: a) (t :: a). ((Apply (Apply MinSym0 t) t :: a) ~ Apply (Apply Min_6989586621679316827Sym0 t) t) => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) #

Instances

SOrd Bool #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd Ordering #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd Nat #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd Symbol #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd () #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd Void #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd [a]) => SOrd [a] #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
SOrd a => SOrd (Maybe a) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd [a]) => SOrd (NonEmpty a) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b) => SOrd (Either a b) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b) => SOrd (a, b) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #

type family Comparing (a :: TyFun b a -> Type) (a :: b) (a :: b) :: Ordering where ... #

Equations

Comparing p x y = Apply (Apply CompareSym0 (Apply p x)) (Apply p y)

sComparing :: forall (t :: TyFun b a -> Type) (t :: b) (t :: b). SOrd a => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ComparingSym0 t) t) t :: Ordering) #

thenCmp returns its second argument if its first is EQ; otherwise, it returns its first argument.

thenCmp :: Ordering -> Ordering -> Ordering #

type family ThenCmp (a :: Ordering) (a :: Ordering) :: Ordering where ... #

Equations

ThenCmp EQ x = x
ThenCmp LT _ = LTSym0
ThenCmp GT _ = GTSym0

sThenCmp :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering) #

data family Sing (a :: k) #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> *) #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods compare :: Sing a -> Sing a -> Ordering # (<) :: Sing a -> Sing a -> Bool # (<=) :: Sing a -> Sing a -> Bool # (>) :: Sing a -> Sing a -> Bool # (>=) :: Sing a -> Sing a -> Bool # max :: Sing a -> Sing a -> Sing a # min :: Sing a -> Sing a -> Sing a #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) #
Instance details Defined in Data.Singletons.TypeRepStar Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (z :: Bool) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Bool) where SFalse :: Sing False STrue :: Sing True
data Sing (z :: Ordering) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Ordering) where SLT :: Sing LT SEQ :: Sing EQ SGT :: Sing GT
data Sing (a :: Type) #
Instance details Defined in Data.Singletons.TypeRepStar data Sing (a :: Type) = STypeRep (TypeRep a)
data Sing (n :: Nat) #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: Sing n
data Sing (n :: Symbol) #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: Sing n
data Sing (z :: ()) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: ()) where STuple0 :: Sing ()
data Sing (z :: Void) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Void)
data Sing (z :: [a]) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: [a]) where SNil :: Sing ([] :: [k]) SCons :: Sing (n ': n)
data Sing (z :: Maybe a) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Maybe a) where SNothing :: Sing (Nothing :: Maybe a) SJust :: Sing (Just n)
data Sing (z :: NonEmpty a) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: NonEmpty a) where (:%\|) :: Sing (n :\| n)
data Sing (z :: Either a b) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Either a b) where SLeft :: Sing (Left n :: Either a b) SRight :: Sing (Right n :: Either a b)
data Sing (z :: (a, b)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b)) where STuple2 :: Sing ((,) n n)
data Sing (f :: k1 ~> k2) #
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (z :: (a, b, c)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c)) where STuple3 :: Sing ((,,) n n n)
data Sing (z :: (a, b, c, d)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d)) where STuple4 :: Sing ((,,,) n n n n)
data Sing (z :: (a, b, c, d, e)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e)) where STuple5 :: Sing ((,,,,) n n n n n)
data Sing (z :: (a, b, c, d, e, f)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f)) where STuple6 :: Sing ((,,,,,) n n n n n n)
data Sing (z :: (a, b, c, d, e, f, g)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: (a, b, c, d, e, f, g)) where STuple7 :: Sing ((,,,,,,) n n n n n n n)

Defunctionalization symbols

data ThenCmpSym0 (l :: TyFun Ordering (TyFun Ordering Ordering -> Type)) #

Instances

SuppressUnusedWarnings ThenCmpSym0 #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ThenCmpSym0 (l :: Ordering) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ThenCmpSym0 (l :: Ordering) = ThenCmpSym1 l

data ThenCmpSym1 (l :: Ordering) (l :: TyFun Ordering Ordering) #

Instances

SuppressUnusedWarnings ThenCmpSym1 #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (ThenCmpSym1 l1 :: TyFun Ordering Ordering -> *) (l2 :: Ordering) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ThenCmpSym1 l1 :: TyFun Ordering Ordering -> *) (l2 :: Ordering) = ThenCmp l1 l2

type ThenCmpSym2 (t :: Ordering) (t :: Ordering) = ThenCmp t t #

type LTSym0 = LT #

type EQSym0 = EQ #

type GTSym0 = GT #

data CompareSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Ordering -> Type)) #

Instances

SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Ordering -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (CompareSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Ordering -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Ordering -> Type) -> *) (l :: a6989586621679315171) = CompareSym1 l

data CompareSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 Ordering) #

Instances

SuppressUnusedWarnings (CompareSym1 :: a6989586621679315171 -> TyFun a6989586621679315171 Ordering -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) = Compare l1 l2

type CompareSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Compare t t #

data (<@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type)) #

Instances

SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((<@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) = (<@#@$$) l

data (l :: a6989586621679315171) <@#@$$ (l :: TyFun a6989586621679315171 Bool) #

Instances

SuppressUnusedWarnings ((<@#@$$) :: a6989586621679315171 -> TyFun a6989586621679315171 Bool -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 < l2

type (<@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (<) t t #

data (<=@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type)) #

Instances

SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((<=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) = (<=@#@$$) l

data (l :: a6989586621679315171) <=@#@$$ (l :: TyFun a6989586621679315171 Bool) #

Instances

SuppressUnusedWarnings ((<=@#@$$) :: a6989586621679315171 -> TyFun a6989586621679315171 Bool -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 <= l2

type (<=@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (<=) t t #

data (>@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type)) #

Instances

SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((>@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) = (>@#@$$) l

data (l :: a6989586621679315171) >@#@$$ (l :: TyFun a6989586621679315171 Bool) #

Instances

SuppressUnusedWarnings ((>@#@$$) :: a6989586621679315171 -> TyFun a6989586621679315171 Bool -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 > l2

type (>@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (>) t t #

data (>=@#@$) (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type)) #

Instances

SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((>=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>=@#@$) :: TyFun a6989586621679315171 (TyFun a6989586621679315171 Bool -> Type) -> *) (l :: a6989586621679315171) = (>=@#@$$) l

data (l :: a6989586621679315171) >=@#@$$ (l :: TyFun a6989586621679315171 Bool) #

Instances

SuppressUnusedWarnings ((>=@#@$$) :: a6989586621679315171 -> TyFun a6989586621679315171 Bool -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 >= l2

type (>=@#@$$$) (t :: a6989586621679315171) (t :: a6989586621679315171) = (>=) t t #

data MaxSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type)) #

Instances

SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (MaxSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MaxSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) (l :: a6989586621679315171) = MaxSym1 l

data MaxSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 a6989586621679315171) #

Instances

SuppressUnusedWarnings (MaxSym1 :: a6989586621679315171 -> TyFun a6989586621679315171 a6989586621679315171 -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) = Max l1 l2

type MaxSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Max t t #

data MinSym0 (l :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type)) #

Instances

SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (MinSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) (l :: a6989586621679315171) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MinSym0 :: TyFun a6989586621679315171 (TyFun a6989586621679315171 a6989586621679315171 -> Type) -> *) (l :: a6989586621679315171) = MinSym1 l

data MinSym1 (l :: a6989586621679315171) (l :: TyFun a6989586621679315171 a6989586621679315171) #

Instances

SuppressUnusedWarnings (MinSym1 :: a6989586621679315171 -> TyFun a6989586621679315171 a6989586621679315171 -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) = Min l1 l2

type MinSym2 (t :: a6989586621679315171) (t :: a6989586621679315171) = Min t t #

data ComparingSym0 (l :: TyFun (TyFun b6989586621679315161 a6989586621679315160 -> Type) (TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (ComparingSym0 :: TyFun (TyFun b6989586621679315161 a6989586621679315160 -> Type) (TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym0 :: TyFun (TyFun b6989586621679315161 a6989586621679315160 -> Type) (TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> Type) -> *) (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym0 :: TyFun (TyFun b6989586621679315161 a6989586621679315160 -> Type) (TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> Type) -> *) (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) = ComparingSym1 l

data ComparingSym1 (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (l :: TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type)) #

Instances

SuppressUnusedWarnings (ComparingSym1 :: (TyFun b6989586621679315161 a6989586621679315160 -> Type) -> TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym1 l1 :: TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> *) (l2 :: b6989586621679315161) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym1 l1 :: TyFun b6989586621679315161 (TyFun b6989586621679315161 Ordering -> Type) -> *) (l2 :: b6989586621679315161) = ComparingSym2 l1 l2

data ComparingSym2 (l :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (l :: b6989586621679315161) (l :: TyFun b6989586621679315161 Ordering) #

Instances

SuppressUnusedWarnings (ComparingSym2 :: (TyFun b6989586621679315161 a6989586621679315160 -> Type) -> b6989586621679315161 -> TyFun b6989586621679315161 Ordering -> *) #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym2 l1 l2 :: TyFun b Ordering -> *) (l3 :: b) #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym2 l1 l2 :: TyFun b Ordering -> *) (l3 :: b) = Comparing l1 l2 l3

type ComparingSym3 (t :: TyFun b6989586621679315161 a6989586621679315160 -> Type) (t :: b6989586621679315161) (t :: b6989586621679315161) = Comparing t t t #