Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Ord.Singletons

Contents

Defunctionalization symbols
Orphan instances

Description

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

Synopsis

class POrd a 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
- 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)
- (%<=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool)
- (%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool)
- (%>=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool)
- 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)
type family Comparing (a :: (~>) b a) (a :: b) (a :: b) :: Ordering where ...
sComparing :: forall b a (t :: (~>) b a) (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)
type family Sing :: k -> Type
data SOrdering :: Ordering -> Type where
- SLT :: SOrdering ('LT :: Ordering)
- SEQ :: SOrdering ('EQ :: Ordering)
- SGT :: SOrdering ('GT :: Ordering)
data SDown :: forall (a :: Type). Down a -> Type where
- SDown :: forall (a :: Type) (n :: a). (Sing n) -> SDown ('Down n :: Down (a :: Type))
type family GetDown (a :: Down (a :: Type)) :: a where ...
sGetDown :: forall (a :: Type) (t :: Down (a :: Type)). Sing t -> Sing (Apply GetDownSym0 t :: a)
data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering)
data ThenCmpSym1 (a6989586621679184996 :: Ordering) :: (~>) Ordering Ordering
type family ThenCmpSym2 (a6989586621679184996 :: Ordering) (a6989586621679184997 :: Ordering) :: Ordering where ...
type family LTSym0 :: Ordering where ...
type family EQSym0 :: Ordering where ...
type family GTSym0 :: Ordering where ...
data CompareSym0 :: (~>) a ((~>) a Ordering)
data CompareSym1 (a6989586621679185012 :: a) :: (~>) a Ordering
type family CompareSym2 (a6989586621679185012 :: a) (a6989586621679185013 :: a) :: Ordering where ...
data (<@#@$) :: (~>) a ((~>) a Bool)
data (<@#@$$) (a6989586621679185017 :: a) :: (~>) a Bool
type family (a6989586621679185017 :: a) <@#@$$$ (a6989586621679185018 :: a) :: Bool where ...
data (<=@#@$) :: (~>) a ((~>) a Bool)
data (<=@#@$$) (a6989586621679185022 :: a) :: (~>) a Bool
type family (a6989586621679185022 :: a) <=@#@$$$ (a6989586621679185023 :: a) :: Bool where ...
data (>@#@$) :: (~>) a ((~>) a Bool)
data (>@#@$$) (a6989586621679185027 :: a) :: (~>) a Bool
type family (a6989586621679185027 :: a) >@#@$$$ (a6989586621679185028 :: a) :: Bool where ...
data (>=@#@$) :: (~>) a ((~>) a Bool)
data (>=@#@$$) (a6989586621679185032 :: a) :: (~>) a Bool
type family (a6989586621679185032 :: a) >=@#@$$$ (a6989586621679185033 :: a) :: Bool where ...
data MaxSym0 :: (~>) a ((~>) a a)
data MaxSym1 (a6989586621679185037 :: a) :: (~>) a a
type family MaxSym2 (a6989586621679185037 :: a) (a6989586621679185038 :: a) :: a where ...
data MinSym0 :: (~>) a ((~>) a a)
data MinSym1 (a6989586621679185042 :: a) :: (~>) a a
type family MinSym2 (a6989586621679185042 :: a) (a6989586621679185043 :: a) :: a where ...
data ComparingSym0 :: (~>) ((~>) b a) ((~>) b ((~>) b Ordering))
data ComparingSym1 (a6989586621679185003 :: (~>) b a) :: (~>) b ((~>) b Ordering)
data ComparingSym2 (a6989586621679185003 :: (~>) b a) (a6989586621679185004 :: b) :: (~>) b Ordering
type family ComparingSym3 (a6989586621679185003 :: (~>) b a) (a6989586621679185004 :: b) (a6989586621679185005 :: b) :: Ordering where ...
data DownSym0 :: (~>) a (Down (a :: Type))
type family DownSym1 (a6989586621679195717 :: a) :: Down (a :: Type) where ...
data GetDownSym0 :: (~>) (Down (a :: Type)) a
type family GetDownSym1 (a6989586621679195720 :: Down (a :: Type)) :: a where ...

Documentation

class POrd a Source #

Associated Types

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

type Compare a a = Apply (Apply Compare_6989586621679185046Sym0 a) a

type (arg :: a) < (arg :: a) :: Bool infix 4 Source #

type a < a = Apply (Apply TFHelper_6989586621679185067Sym0 a) a

type (arg :: a) <= (arg :: a) :: Bool infix 4 Source #

type a <= a = Apply (Apply TFHelper_6989586621679185083Sym0 a) a

type (arg :: a) > (arg :: a) :: Bool infix 4 Source #

type a > a = Apply (Apply TFHelper_6989586621679185099Sym0 a) a

type (arg :: a) >= (arg :: a) :: Bool infix 4 Source #

type a >= a = Apply (Apply TFHelper_6989586621679185115Sym0 a) a

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

type Max a a = Apply (Apply Max_6989586621679185131Sym0 a) a

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

type Min a a = Apply (Apply Min_6989586621679185147Sym0 a) a

Instances

Instances details

POrd All Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Any Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Void Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Ordering Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Natural Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd () Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Bool Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Char Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Identity a) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (First a) Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Last a) Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Down a) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (First a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Last a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Max a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Min a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (WrappedMonoid m) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Dual a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Product a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Sum a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (NonEmpty a) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Maybe a) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd [a] Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Either a b) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Proxy s) Source #
Instance details Defined in Data.Proxy.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Arg a b) Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (Const a b) Source #
Instance details Defined in Data.Functor.Const.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e, f) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
POrd (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #

class SEq a => SOrd a where Source #

Minimal complete definition

Nothing

Methods

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

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

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

default (%<) :: forall (t :: a) (t :: a). (Apply (Apply (<@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679185067Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t :: Bool) Source #

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

default (%<=) :: forall (t :: a) (t :: a). (Apply (Apply (<=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679185083Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t :: Bool) Source #

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

default (%>) :: forall (t :: a) (t :: a). (Apply (Apply (>@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679185099Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t :: Bool) Source #

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

default (%>=) :: forall (t :: a) (t :: a). (Apply (Apply (>=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679185115Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t :: Bool) Source #

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

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

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

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

Instances

Instances details

SOrd Bool => SOrd All Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Bool => SOrd Any Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Void Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Ordering Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Natural Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sCompare :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd () Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Bool Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Char Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sCompare :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods sCompare :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Identity a) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Maybe a) => SOrd (First a) Source #
Instance details Defined in Data.Monoid.Singletons Methods sCompare :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Maybe a) => SOrd (Last a) Source #
Instance details Defined in Data.Monoid.Singletons Methods sCompare :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Down a) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (First a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Last a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Max a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Min a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd m => SOrd (WrappedMonoid m) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Dual a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Product a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Sum a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sCompare :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd [a]) => SOrd (NonEmpty a) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Maybe a) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd [a]) => SOrd [a] Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b) => SOrd (Either a b) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Proxy s) Source #
Instance details Defined in Data.Proxy.Singletons Methods sCompare :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Arg a b) Source #
Instance details Defined in Data.Semigroup.Singletons Methods sCompare :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b) => SOrd (a, b) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Const a b) Source #
Instance details Defined in Data.Functor.Const.Singletons Methods sCompare :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Ord.Singletons Methods sCompare :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

type family Comparing (a :: (~>) b a) (a :: b) (a :: b) :: Ordering where ... Source #

Equations

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

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

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 ... Source #

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) Source #

type family Sing :: k -> Type #

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SBool
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SChar
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Ord.Singletons type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.Base.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Proxy.Singletons type Sing = SProxy :: Proxy t -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons type Sing = SArg :: Arg a b -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Const.Singletons type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Product.Singletons type Sing = SProduct :: Product f g a -> Type
type Sing Source #
Instance details Defined in Data.Functor.Sum.Singletons type Sing = SSum :: Sum f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Compose.Singletons type Sing = SCompose :: Compose f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SOrdering :: Ordering -> Type where Source #

Constructors

SLT :: SOrdering ('LT :: Ordering)
SEQ :: SOrdering ('EQ :: Ordering)
SGT :: SOrdering ('GT :: Ordering)

Instances

Instances details

TestCoercion SOrdering Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testCoercion :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (Coercion a b) #
TestEquality SOrdering Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testEquality :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (a :~: b) #
Show (SOrdering z) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods showsPrec :: Int -> SOrdering z -> ShowS # show :: SOrdering z -> String # showList :: [SOrdering z] -> ShowS #

data SDown :: forall (a :: Type). Down a -> Type where Source #

Constructors

SDown :: forall (a :: Type) (n :: a). (Sing n) -> SDown ('Down n :: Down (a :: Type))

Instances

Instances details

SDecide a => TestCoercion (SDown :: Down a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods testCoercion :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (Coercion a0 b) #
SDecide a => TestEquality (SDown :: Down a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods testEquality :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (a0 :~: b) #

type family GetDown (a :: Down (a :: Type)) :: a where ... Source #

Equations

GetDown ('Down field) = field

sGetDown :: forall (a :: Type) (t :: Down (a :: Type)). Sing t -> Sing (Apply GetDownSym0 t :: a) Source #

Defunctionalization symbols

data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering) Source #

Instances

Instances details

SingI ThenCmpSym0 Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ThenCmpSym0
SuppressUnusedWarnings ThenCmpSym0 Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ThenCmpSym0 (a6989586621679184996 :: Ordering) Source #
Instance details Defined in Data.Ord.Singletons type Apply ThenCmpSym0 (a6989586621679184996 :: Ordering) = ThenCmpSym1 a6989586621679184996

data ThenCmpSym1 (a6989586621679184996 :: Ordering) :: (~>) Ordering Ordering Source #

Instances

Instances details

SingI1 ThenCmpSym1 Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ThenCmpSym1 x)
SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (ThenCmpSym1 d)
SuppressUnusedWarnings (ThenCmpSym1 a6989586621679184996 :: TyFun Ordering Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ThenCmpSym1 a6989586621679184996 :: TyFun Ordering Ordering -> Type) (a6989586621679184997 :: Ordering) Source #
Instance details Defined in Data.Ord.Singletons type Apply (ThenCmpSym1 a6989586621679184996 :: TyFun Ordering Ordering -> Type) (a6989586621679184997 :: Ordering) = ThenCmp a6989586621679184996 a6989586621679184997

type family ThenCmpSym2 (a6989586621679184996 :: Ordering) (a6989586621679184997 :: Ordering) :: Ordering where ... Source #

Equations

ThenCmpSym2 a6989586621679184996 a6989586621679184997 = ThenCmp a6989586621679184996 a6989586621679184997

type family LTSym0 :: Ordering where ... Source #

Equations

LTSym0 = 'LT

type family EQSym0 :: Ordering where ... Source #

Equations

EQSym0 = 'EQ

type family GTSym0 :: Ordering where ... Source #

Equations

GTSym0 = 'GT

data CompareSym0 :: (~>) a ((~>) a Ordering) Source #

Instances

Instances details

SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing CompareSym0
SuppressUnusedWarnings (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679185012 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679185012 :: a) = CompareSym1 a6989586621679185012

data CompareSym1 (a6989586621679185012 :: a) :: (~>) a Ordering Source #

Instances

Instances details

SOrd a => SingI1 (CompareSym1 :: a -> TyFun a Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (CompareSym1 x)
(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (CompareSym1 d)
SuppressUnusedWarnings (CompareSym1 a6989586621679185012 :: TyFun a Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (CompareSym1 a6989586621679185012 :: TyFun a Ordering -> Type) (a6989586621679185013 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (CompareSym1 a6989586621679185012 :: TyFun a Ordering -> Type) (a6989586621679185013 :: a) = Compare a6989586621679185012 a6989586621679185013

type family CompareSym2 (a6989586621679185012 :: a) (a6989586621679185013 :: a) :: Ordering where ... Source #

Equations

CompareSym2 a6989586621679185012 a6989586621679185013 = Compare a6989586621679185012 a6989586621679185013

data (<@#@$) :: (~>) a ((~>) a Bool) infix 4 Source #

Instances

Instances details

SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (<@#@$)
SuppressUnusedWarnings ((<@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185017 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((<@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185017 :: a) = (<@#@$$) a6989586621679185017

data (<@#@$$) (a6989586621679185017 :: a) :: (~>) a Bool infix 4 Source #

Instances

Instances details

SOrd a => SingI1 ((<@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<@#@$$) x)
(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ((<@#@$$) d)
SuppressUnusedWarnings ((<@#@$$) a6989586621679185017 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<@#@$$) a6989586621679185017 :: TyFun a Bool -> Type) (a6989586621679185018 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((<@#@$$) a6989586621679185017 :: TyFun a Bool -> Type) (a6989586621679185018 :: a) = a6989586621679185017 < a6989586621679185018

type family (a6989586621679185017 :: a) <@#@$$$ (a6989586621679185018 :: a) :: Bool where ... infix 4 Source #

Equations

a6989586621679185017 <@#@$$$ a6989586621679185018 = (<) a6989586621679185017 a6989586621679185018

data (<=@#@$) :: (~>) a ((~>) a Bool) infix 4 Source #

Instances

Instances details

SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (<=@#@$)
SuppressUnusedWarnings ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185022 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185022 :: a) = (<=@#@$$) a6989586621679185022

data (<=@#@$$) (a6989586621679185022 :: a) :: (~>) a Bool infix 4 Source #

Instances

Instances details

SOrd a => SingI1 ((<=@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<=@#@$$) x)
(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ((<=@#@$$) d)
SuppressUnusedWarnings ((<=@#@$$) a6989586621679185022 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<=@#@$$) a6989586621679185022 :: TyFun a Bool -> Type) (a6989586621679185023 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((<=@#@$$) a6989586621679185022 :: TyFun a Bool -> Type) (a6989586621679185023 :: a) = a6989586621679185022 <= a6989586621679185023

type family (a6989586621679185022 :: a) <=@#@$$$ (a6989586621679185023 :: a) :: Bool where ... infix 4 Source #

Equations

a6989586621679185022 <=@#@$$$ a6989586621679185023 = (<=) a6989586621679185022 a6989586621679185023

data (>@#@$) :: (~>) a ((~>) a Bool) infix 4 Source #

Instances

Instances details

SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (>@#@$)
SuppressUnusedWarnings ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((>@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185027 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((>@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185027 :: a) = (>@#@$$) a6989586621679185027

data (>@#@$$) (a6989586621679185027 :: a) :: (~>) a Bool infix 4 Source #

Instances

Instances details

SOrd a => SingI1 ((>@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((>@#@$$) x)
(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ((>@#@$$) d)
SuppressUnusedWarnings ((>@#@$$) a6989586621679185027 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((>@#@$$) a6989586621679185027 :: TyFun a Bool -> Type) (a6989586621679185028 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((>@#@$$) a6989586621679185027 :: TyFun a Bool -> Type) (a6989586621679185028 :: a) = a6989586621679185027 > a6989586621679185028

type family (a6989586621679185027 :: a) >@#@$$$ (a6989586621679185028 :: a) :: Bool where ... infix 4 Source #

Equations

a6989586621679185027 >@#@$$$ a6989586621679185028 = (>) a6989586621679185027 a6989586621679185028

data (>=@#@$) :: (~>) a ((~>) a Bool) infix 4 Source #

Instances

Instances details

SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (>=@#@$)
SuppressUnusedWarnings ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185032 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679185032 :: a) = (>=@#@$$) a6989586621679185032

data (>=@#@$$) (a6989586621679185032 :: a) :: (~>) a Bool infix 4 Source #

Instances

Instances details

SOrd a => SingI1 ((>=@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((>=@#@$$) x)
(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ((>=@#@$$) d)
SuppressUnusedWarnings ((>=@#@$$) a6989586621679185032 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((>=@#@$$) a6989586621679185032 :: TyFun a Bool -> Type) (a6989586621679185033 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply ((>=@#@$$) a6989586621679185032 :: TyFun a Bool -> Type) (a6989586621679185033 :: a) = a6989586621679185032 >= a6989586621679185033

type family (a6989586621679185032 :: a) >=@#@$$$ (a6989586621679185033 :: a) :: Bool where ... infix 4 Source #

Equations

a6989586621679185032 >=@#@$$$ a6989586621679185033 = (>=) a6989586621679185032 a6989586621679185033

data MaxSym0 :: (~>) a ((~>) a a) Source #

Instances

Instances details

SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing MaxSym0
SuppressUnusedWarnings (MaxSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (MaxSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679185037 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (MaxSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679185037 :: a) = MaxSym1 a6989586621679185037

data MaxSym1 (a6989586621679185037 :: a) :: (~>) a a Source #

Instances

Instances details

SOrd a => SingI1 (MaxSym1 :: a -> TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (MaxSym1 x)
(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (MaxSym1 d)
SuppressUnusedWarnings (MaxSym1 a6989586621679185037 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (MaxSym1 a6989586621679185037 :: TyFun a a -> Type) (a6989586621679185038 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (MaxSym1 a6989586621679185037 :: TyFun a a -> Type) (a6989586621679185038 :: a) = Max a6989586621679185037 a6989586621679185038

type family MaxSym2 (a6989586621679185037 :: a) (a6989586621679185038 :: a) :: a where ... Source #

Equations

MaxSym2 a6989586621679185037 a6989586621679185038 = Max a6989586621679185037 a6989586621679185038

data MinSym0 :: (~>) a ((~>) a a) Source #

Instances

Instances details

SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing MinSym0
SuppressUnusedWarnings (MinSym0 :: TyFun a (a ~> a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (MinSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679185042 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (MinSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679185042 :: a) = MinSym1 a6989586621679185042

data MinSym1 (a6989586621679185042 :: a) :: (~>) a a Source #

Instances

Instances details

SOrd a => SingI1 (MinSym1 :: a -> TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (MinSym1 x)
(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (MinSym1 d)
SuppressUnusedWarnings (MinSym1 a6989586621679185042 :: TyFun a a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (MinSym1 a6989586621679185042 :: TyFun a a -> Type) (a6989586621679185043 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (MinSym1 a6989586621679185042 :: TyFun a a -> Type) (a6989586621679185043 :: a) = Min a6989586621679185042 a6989586621679185043

type family MinSym2 (a6989586621679185042 :: a) (a6989586621679185043 :: a) :: a where ... Source #

Equations

MinSym2 a6989586621679185042 a6989586621679185043 = Min a6989586621679185042 a6989586621679185043

data ComparingSym0 :: (~>) ((~>) b a) ((~>) b ((~>) b Ordering)) Source #

Instances

Instances details

SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing ComparingSym0
SuppressUnusedWarnings (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) (a6989586621679185003 :: b ~> a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) (a6989586621679185003 :: b ~> a) = ComparingSym1 a6989586621679185003

data ComparingSym1 (a6989586621679185003 :: (~>) b a) :: (~>) b ((~>) b Ordering) Source #

Instances

Instances details

SOrd a => SingI1 (ComparingSym1 :: (b ~> a) -> TyFun b (b ~> Ordering) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ComparingSym1 x)
(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (ComparingSym1 d)
SuppressUnusedWarnings (ComparingSym1 a6989586621679185003 :: TyFun b (b ~> Ordering) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym1 a6989586621679185003 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679185004 :: b) Source #
Instance details Defined in Data.Ord.Singletons type Apply (ComparingSym1 a6989586621679185003 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679185004 :: b) = ComparingSym2 a6989586621679185003 a6989586621679185004

data ComparingSym2 (a6989586621679185003 :: (~>) b a) (a6989586621679185004 :: b) :: (~>) b Ordering Source #

Instances

Instances details

(SOrd a, SingI d) => SingI1 (ComparingSym2 d :: b -> TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (ComparingSym2 d x)
SOrd a => SingI2 (ComparingSym2 :: (b ~> a) -> b -> TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (ComparingSym2 x y)
(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing (ComparingSym2 d1 d2)
SuppressUnusedWarnings (ComparingSym2 a6989586621679185003 a6989586621679185004 :: TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ComparingSym2 a6989586621679185003 a6989586621679185004 :: TyFun b Ordering -> Type) (a6989586621679185005 :: b) Source #
Instance details Defined in Data.Ord.Singletons type Apply (ComparingSym2 a6989586621679185003 a6989586621679185004 :: TyFun b Ordering -> Type) (a6989586621679185005 :: b) = Comparing a6989586621679185003 a6989586621679185004 a6989586621679185005

type family ComparingSym3 (a6989586621679185003 :: (~>) b a) (a6989586621679185004 :: b) (a6989586621679185005 :: b) :: Ordering where ... Source #

Equations

ComparingSym3 a6989586621679185003 a6989586621679185004 a6989586621679185005 = Comparing a6989586621679185003 a6989586621679185004 a6989586621679185005

data DownSym0 :: (~>) a (Down (a :: Type)) Source #

Instances

Instances details

SingI (DownSym0 :: TyFun a (Down a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing DownSym0
SuppressUnusedWarnings (DownSym0 :: TyFun a (Down a) -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (DownSym0 :: TyFun a (Down a) -> Type) (a6989586621679195717 :: a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (DownSym0 :: TyFun a (Down a) -> Type) (a6989586621679195717 :: a) = 'Down a6989586621679195717

type family DownSym1 (a6989586621679195717 :: a) :: Down (a :: Type) where ... Source #

Equations

DownSym1 a6989586621679195717 = 'Down a6989586621679195717

data GetDownSym0 :: (~>) (Down (a :: Type)) a Source #

Instances

Instances details

SingI (GetDownSym0 :: TyFun (Down a) a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods sing :: Sing GetDownSym0
SuppressUnusedWarnings (GetDownSym0 :: TyFun (Down a) a -> Type) Source #
Instance details Defined in Data.Ord.Singletons Methods suppressUnusedWarnings :: () #
type Apply (GetDownSym0 :: TyFun (Down a) a -> Type) (a6989586621679195720 :: Down a) Source #
Instance details Defined in Data.Ord.Singletons type Apply (GetDownSym0 :: TyFun (Down a) a -> Type) (a6989586621679195720 :: Down a) = GetDown a6989586621679195720

type family GetDownSym1 (a6989586621679195720 :: Down (a :: Type)) :: a where ... Source #

Equations

GetDownSym1 a6989586621679195720 = GetDown a6989586621679195720

Orphan instances

SingI1 ('Down :: k1 -> Down k1) Source #
Instance details Methods liftSing :: forall (x :: k10). Sing x -> Sing ('Down0 x)
SingKind a => SingKind (Down a) Source #
Instance details Associated Types type Demote (Down a) = (r :: Type) Methods fromSing :: forall (a0 :: Down a). Sing a0 -> Demote (Down a) toSing :: Demote (Down a) -> SomeSing (Down a)
SDecide a => SDecide (Down a) Source #
Instance details Methods (%~) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
PEq (Down a) Source #
Instance details Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
SEq a => SEq (Down a) Source #
Instance details Methods (%==) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SingI n => SingI ('Down n :: Down a) Source #
Instance details Methods sing :: Sing ('Down0 n)