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

Data.Singletons.Prelude.Ord

Contents

Defunctionalization symbols
Orphan instances

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
- 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 a b (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)
data family Sing :: k -> Type
type SOrdering = (Sing :: Ordering -> Type)
type SDown = (Sing :: Down a -> Type)
data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering)
data ThenCmpSym1 (a6989586621679384037 :: Ordering) :: (~>) Ordering Ordering
type ThenCmpSym2 (a6989586621679384037 :: Ordering) (a6989586621679384038 :: Ordering) = ThenCmp a6989586621679384037 a6989586621679384038
type LTSym0 = LT
type EQSym0 = EQ
type GTSym0 = GT
data CompareSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Ordering)
data CompareSym1 (arg6989586621679373626 :: a6989586621679373532) :: (~>) a6989586621679373532 Ordering
type CompareSym2 (arg6989586621679373626 :: a6989586621679373532) (arg6989586621679373627 :: a6989586621679373532) = Compare arg6989586621679373626 arg6989586621679373627
data (<@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool)
data (<@#@$$) (arg6989586621679373630 :: a6989586621679373532) :: (~>) a6989586621679373532 Bool
type (<@#@$$$) (arg6989586621679373630 :: a6989586621679373532) (arg6989586621679373631 :: a6989586621679373532) = (<) arg6989586621679373630 arg6989586621679373631
data (<=@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool)
data (<=@#@$$) (arg6989586621679373634 :: a6989586621679373532) :: (~>) a6989586621679373532 Bool
type (<=@#@$$$) (arg6989586621679373634 :: a6989586621679373532) (arg6989586621679373635 :: a6989586621679373532) = (<=) arg6989586621679373634 arg6989586621679373635
data (>@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool)
data (>@#@$$) (arg6989586621679373638 :: a6989586621679373532) :: (~>) a6989586621679373532 Bool
type (>@#@$$$) (arg6989586621679373638 :: a6989586621679373532) (arg6989586621679373639 :: a6989586621679373532) = (>) arg6989586621679373638 arg6989586621679373639
data (>=@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool)
data (>=@#@$$) (arg6989586621679373642 :: a6989586621679373532) :: (~>) a6989586621679373532 Bool
type (>=@#@$$$) (arg6989586621679373642 :: a6989586621679373532) (arg6989586621679373643 :: a6989586621679373532) = (>=) arg6989586621679373642 arg6989586621679373643
data MaxSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 a6989586621679373532)
data MaxSym1 (arg6989586621679373646 :: a6989586621679373532) :: (~>) a6989586621679373532 a6989586621679373532
type MaxSym2 (arg6989586621679373646 :: a6989586621679373532) (arg6989586621679373647 :: a6989586621679373532) = Max arg6989586621679373646 arg6989586621679373647
data MinSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 a6989586621679373532)
data MinSym1 (arg6989586621679373650 :: a6989586621679373532) :: (~>) a6989586621679373532 a6989586621679373532
type MinSym2 (arg6989586621679373650 :: a6989586621679373532) (arg6989586621679373651 :: a6989586621679373532) = Min arg6989586621679373650 arg6989586621679373651
data ComparingSym0 :: forall a6989586621679373521 b6989586621679373522. (~>) ((~>) b6989586621679373522 a6989586621679373521) ((~>) b6989586621679373522 ((~>) b6989586621679373522 Ordering))
data ComparingSym1 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) :: (~>) b6989586621679373522 ((~>) b6989586621679373522 Ordering)
data ComparingSym2 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) (a6989586621679373618 :: b6989586621679373522) :: (~>) b6989586621679373522 Ordering
type ComparingSym3 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) (a6989586621679373618 :: b6989586621679373522) (a6989586621679373619 :: b6989586621679373522) = Comparing a6989586621679373617 a6989586621679373618 a6989586621679373619
data DownSym0 :: forall (a6989586621679086132 :: Type). (~>) a6989586621679086132 (Down (a6989586621679086132 :: Type))
type DownSym1 (t6989586621679382719 :: a6989586621679086132) = Down t6989586621679382719

Documentation

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

Associated Types

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

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

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

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

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

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

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

Instances

POrd Bool Source #
Instance details Defined in Data.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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 Nat Source #
Instance details Defined in Data.Singletons.TypeLits.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 Data.Singletons.TypeLits.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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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 All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 [a] Source #
Instance details Defined in Data.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 (Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Ord 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.Singletons.Prelude.Monoid 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.Singletons.Prelude.Monoid 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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 (Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Semigroup 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Const 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord 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 #

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

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

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

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

sMax :: forall (t :: a) (t :: a). 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 #

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

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

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

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

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

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

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

Instances

SOrd Bool Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Ordering Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Nat Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Symbol Source #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd () Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Void Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Bool => SOrd All Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd Bool => SOrd Any Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd [a]) => SOrd [a] Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd m => SOrd (WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Maybe a) => SOrd (Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Maybe a) => SOrd (First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd (Maybe a) => SOrd (Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd [a]) => SOrd (NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
(SOrd a, SOrd b) => SOrd (a, b) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #
SOrd a => SOrd (Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source # sMin :: 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 a b (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 Source #

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 #

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type) Source #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> Type) Source #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE 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) Source #
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) Source #
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) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) Source #
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) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
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) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) Source #
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) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing m => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (a :: Bool) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol) Source #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ()) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Void) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (a :: PErrorMessage) Source #
Instance details Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t) SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol) (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2) (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)
data Sing (b :: [a]) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall k (b :: [k]). Sing ([] :: [k]) SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)
data Sing (b :: Maybe a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (a :: TYPE rep) 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 -> Type` 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.TypeRepTYPE data Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a) Source #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :\| n)
data Sing (c :: Either a b) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)
data Sing (c :: Arg a b) Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)
data Sing (f :: k1 ~> k2) Source #
Instance details Defined in Data.Singletons.Internal data Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (d :: (a, b, c)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)
data Sing (c :: Const a b) Source #
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)
data Sing (e :: (a, b, c, d)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)
data Sing (f :: (a, b, c, d, e)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)
data Sing (g :: (a, b, c, d, e, f)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)
data Sing (h :: (a, b, c, d, e, f, g)) Source #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

type SOrdering = (Sing :: Ordering -> Type) Source #

type SDown = (Sing :: Down a -> Type) Source #

Defunctionalization symbols

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

Instances

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

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

Instances

SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ThenCmpSym1 d) Source #
SuppressUnusedWarnings (ThenCmpSym1 a6989586621679384037 :: TyFun Ordering Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ThenCmpSym1 a6989586621679384037 :: TyFun Ordering Ordering -> Type) (a6989586621679384038 :: Ordering) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ThenCmpSym1 a6989586621679384037 :: TyFun Ordering Ordering -> Type) (a6989586621679384038 :: Ordering) = ThenCmp a6989586621679384037 a6989586621679384038

type ThenCmpSym2 (a6989586621679384037 :: Ordering) (a6989586621679384038 :: Ordering) = ThenCmp a6989586621679384037 a6989586621679384038 Source #

type LTSym0 = LT Source #

type EQSym0 = EQ Source #

type GTSym0 = GT Source #

data CompareSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Ordering) Source #

Instances

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

data CompareSym1 (arg6989586621679373626 :: a6989586621679373532) :: (~>) a6989586621679373532 Ordering Source #

Instances

(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (CompareSym1 d) Source #
SuppressUnusedWarnings (CompareSym1 arg6989586621679373626 :: TyFun a6989586621679373532 Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (CompareSym1 arg6989586621679373626 :: TyFun a Ordering -> Type) (arg6989586621679373627 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym1 arg6989586621679373626 :: TyFun a Ordering -> Type) (arg6989586621679373627 :: a) = Compare arg6989586621679373626 arg6989586621679373627

type CompareSym2 (arg6989586621679373626 :: a6989586621679373532) (arg6989586621679373627 :: a6989586621679373532) = Compare arg6989586621679373626 arg6989586621679373627 Source #

data (<@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool) infix 4 Source #

Instances

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

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

Instances

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

type (<@#@$$$) (arg6989586621679373630 :: a6989586621679373532) (arg6989586621679373631 :: a6989586621679373532) = (<) arg6989586621679373630 arg6989586621679373631 Source #

data (<=@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool) infix 4 Source #

Instances

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

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

Instances

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

type (<=@#@$$$) (arg6989586621679373634 :: a6989586621679373532) (arg6989586621679373635 :: a6989586621679373532) = (<=) arg6989586621679373634 arg6989586621679373635 Source #

data (>@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool) infix 4 Source #

Instances

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

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

Instances

(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>@#@$$) d) Source #
SuppressUnusedWarnings ((>@#@$$) arg6989586621679373638 :: TyFun a6989586621679373532 Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((>@#@$$) arg6989586621679373638 :: TyFun a Bool -> Type) (arg6989586621679373639 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>@#@$$) arg6989586621679373638 :: TyFun a Bool -> Type) (arg6989586621679373639 :: a) = arg6989586621679373638 > arg6989586621679373639

type (>@#@$$$) (arg6989586621679373638 :: a6989586621679373532) (arg6989586621679373639 :: a6989586621679373532) = (>) arg6989586621679373638 arg6989586621679373639 Source #

data (>=@#@$) :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 Bool) infix 4 Source #

Instances

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

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

Instances

(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>=@#@$$) d) Source #
SuppressUnusedWarnings ((>=@#@$$) arg6989586621679373642 :: TyFun a6989586621679373532 Bool -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((>=@#@$$) arg6989586621679373642 :: TyFun a Bool -> Type) (arg6989586621679373643 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>=@#@$$) arg6989586621679373642 :: TyFun a Bool -> Type) (arg6989586621679373643 :: a) = arg6989586621679373642 >= arg6989586621679373643

type (>=@#@$$$) (arg6989586621679373642 :: a6989586621679373532) (arg6989586621679373643 :: a6989586621679373532) = (>=) arg6989586621679373642 arg6989586621679373643 Source #

data MaxSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 a6989586621679373532) Source #

Instances

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

data MaxSym1 (arg6989586621679373646 :: a6989586621679373532) :: (~>) a6989586621679373532 a6989586621679373532 Source #

Instances

(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MaxSym1 d) Source #
SuppressUnusedWarnings (MaxSym1 arg6989586621679373646 :: TyFun a6989586621679373532 a6989586621679373532 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MaxSym1 arg6989586621679373646 :: TyFun a a -> Type) (arg6989586621679373647 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MaxSym1 arg6989586621679373646 :: TyFun a a -> Type) (arg6989586621679373647 :: a) = Max arg6989586621679373646 arg6989586621679373647

type MaxSym2 (arg6989586621679373646 :: a6989586621679373532) (arg6989586621679373647 :: a6989586621679373532) = Max arg6989586621679373646 arg6989586621679373647 Source #

data MinSym0 :: forall a6989586621679373532. (~>) a6989586621679373532 ((~>) a6989586621679373532 a6989586621679373532) Source #

Instances

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

data MinSym1 (arg6989586621679373650 :: a6989586621679373532) :: (~>) a6989586621679373532 a6989586621679373532 Source #

Instances

(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MinSym1 d) Source #
SuppressUnusedWarnings (MinSym1 arg6989586621679373650 :: TyFun a6989586621679373532 a6989586621679373532 -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MinSym1 arg6989586621679373650 :: TyFun a a -> Type) (arg6989586621679373651 :: a) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MinSym1 arg6989586621679373650 :: TyFun a a -> Type) (arg6989586621679373651 :: a) = Min arg6989586621679373650 arg6989586621679373651

type MinSym2 (arg6989586621679373650 :: a6989586621679373532) (arg6989586621679373651 :: a6989586621679373532) = Min arg6989586621679373650 arg6989586621679373651 Source #

data ComparingSym0 :: forall a6989586621679373521 b6989586621679373522. (~>) ((~>) b6989586621679373522 a6989586621679373521) ((~>) b6989586621679373522 ((~>) b6989586621679373522 Ordering)) Source #

Instances

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

data ComparingSym1 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) :: (~>) b6989586621679373522 ((~>) b6989586621679373522 Ordering) Source #

Instances

(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym1 d) Source #
SuppressUnusedWarnings (ComparingSym1 a6989586621679373617 :: TyFun b6989586621679373522 (b6989586621679373522 ~> Ordering) -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ComparingSym1 a6989586621679373617 :: TyFun b6989586621679373522 (b6989586621679373522 ~> Ordering) -> Type) (a6989586621679373618 :: b6989586621679373522) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym1 a6989586621679373617 :: TyFun b6989586621679373522 (b6989586621679373522 ~> Ordering) -> Type) (a6989586621679373618 :: b6989586621679373522) = ComparingSym2 a6989586621679373617 a6989586621679373618

data ComparingSym2 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) (a6989586621679373618 :: b6989586621679373522) :: (~>) b6989586621679373522 Ordering Source #

Instances

(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym2 d1 d2) Source #
SuppressUnusedWarnings (ComparingSym2 a6989586621679373618 a6989586621679373617 :: TyFun b6989586621679373522 Ordering -> Type) Source #
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ComparingSym2 a6989586621679373618 a6989586621679373617 :: TyFun b Ordering -> Type) (a6989586621679373619 :: b) Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym2 a6989586621679373618 a6989586621679373617 :: TyFun b Ordering -> Type) (a6989586621679373619 :: b) = Comparing a6989586621679373618 a6989586621679373617 a6989586621679373619

type ComparingSym3 (a6989586621679373617 :: (~>) b6989586621679373522 a6989586621679373521) (a6989586621679373618 :: b6989586621679373522) (a6989586621679373619 :: b6989586621679373522) = Comparing a6989586621679373617 a6989586621679373618 a6989586621679373619 Source #

data DownSym0 :: forall (a6989586621679086132 :: Type). (~>) a6989586621679086132 (Down (a6989586621679086132 :: Type)) Source #

Instances

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

type DownSym1 (t6989586621679382719 :: a6989586621679086132) = Down t6989586621679382719 Source #

Orphan instances

SingKind a => SingKind (Down a) Source #
Instance details Associated Types type Demote (Down a) = (r :: Type) Source # Methods fromSing :: Sing a0 -> Demote (Down a) Source # toSing :: Demote (Down a) -> SomeSing (Down a) Source #
SDecide a => SDecide (Down a) Source #
Instance details Methods (%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
PEq (Down a) Source #
Instance details Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq a => SEq (Down a) Source #
Instance details Methods (%==) :: Sing a0 -> Sing b -> Sing (a0 == b) Source # (%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b) Source #
SingI n => SingI (Down n :: Down a) Source #
Instance details Methods sing :: Sing (Down0 n) Source #
SingI (TyCon1 (Down :: a -> Down a) :: a ~> Down a) Source #
Instance details Methods sing :: Sing (TyCon1 Down0) Source #