singletons-2.6: A framework for generating singleton types

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 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 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
  - SEQ :: SOrdering 'EQ
  - SGT :: SOrdering 'GT
- data SDown :: forall a. Down a -> Type where
  - SDown :: forall a (n :: a). (Sing (n :: a)) -> SDown ('Down n)
- data ThenCmpSym0 :: (~>) Ordering ((~>) Ordering Ordering)
- data ThenCmpSym1 (a6989586621679400187 :: Ordering) :: (~>) Ordering Ordering
- type ThenCmpSym2 (a6989586621679400187 :: Ordering) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188
- type LTSym0 = 'LT
- type EQSym0 = 'EQ
- type GTSym0 = 'GT
- data CompareSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Ordering)
- data CompareSym1 (arg6989586621679389843 :: a6989586621679389754) :: (~>) a6989586621679389754 Ordering
- type CompareSym2 (arg6989586621679389843 :: a6989586621679389754) (arg6989586621679389844 :: a6989586621679389754) = Compare arg6989586621679389843 arg6989586621679389844
- data (<@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (<@#@$$) (arg6989586621679389847 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (<@#@$$$) (arg6989586621679389847 :: a6989586621679389754) (arg6989586621679389848 :: a6989586621679389754) = (<) arg6989586621679389847 arg6989586621679389848
- data (<=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (<=@#@$$) (arg6989586621679389851 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (<=@#@$$$) (arg6989586621679389851 :: a6989586621679389754) (arg6989586621679389852 :: a6989586621679389754) = (<=) arg6989586621679389851 arg6989586621679389852
- data (>@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (>@#@$$) (arg6989586621679389855 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (>@#@$$$) (arg6989586621679389855 :: a6989586621679389754) (arg6989586621679389856 :: a6989586621679389754) = (>) arg6989586621679389855 arg6989586621679389856
- data (>=@#@$) :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 Bool)
- data (>=@#@$$) (arg6989586621679389859 :: a6989586621679389754) :: (~>) a6989586621679389754 Bool
- type (>=@#@$$$) (arg6989586621679389859 :: a6989586621679389754) (arg6989586621679389860 :: a6989586621679389754) = (>=) arg6989586621679389859 arg6989586621679389860
- data MaxSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754)
- data MaxSym1 (arg6989586621679389863 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754
- type MaxSym2 (arg6989586621679389863 :: a6989586621679389754) (arg6989586621679389864 :: a6989586621679389754) = Max arg6989586621679389863 arg6989586621679389864
- data MinSym0 :: forall a6989586621679389754. (~>) a6989586621679389754 ((~>) a6989586621679389754 a6989586621679389754)
- data MinSym1 (arg6989586621679389867 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754
- type MinSym2 (arg6989586621679389867 :: a6989586621679389754) (arg6989586621679389868 :: a6989586621679389754) = Min arg6989586621679389867 arg6989586621679389868
- data ComparingSym0 :: forall b6989586621679389744 a6989586621679389743. (~>) ((~>) b6989586621679389744 a6989586621679389743) ((~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering))
- data ComparingSym1 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) :: (~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering)
- data ComparingSym2 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) :: (~>) b6989586621679389744 Ordering
- type ComparingSym3 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) (a6989586621679389836 :: b6989586621679389744) = Comparing a6989586621679389834 a6989586621679389835 a6989586621679389836
- data DownSym0 :: forall (a6989586621679089884 :: Type). (~>) a6989586621679089884 (Down (a6989586621679089884 :: Type))
- type DownSym1 (t6989586621679398850 :: a6989586621679089884) = 'Down t6989586621679398850

# Documentation

class POrd (a :: Type) Source #

Associated Types

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

type Compare a a = Apply (Apply Compare_6989586621679389873Sym0 a) a Source #

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

type (<) a a = Apply (Apply TFHelper_6989586621679389897Sym0 a) a Source #

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

type (<=) a a = Apply (Apply TFHelper_6989586621679389915Sym0 a) a Source #

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

type (>) a a = Apply (Apply TFHelper_6989586621679389933Sym0 a) a Source #

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

type (>=) a a = Apply (Apply TFHelper_6989586621679389951Sym0 a) a Source #

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

type Max a a = Apply (Apply Max_6989586621679389969Sym0 a) a Source #

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

type Min a a = Apply (Apply Min_6989586621679389987Sym0 a) a Source #

#### Instances

Instances details

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

default sCompare :: forall (t :: a) (t :: a). (Apply (Apply CompareSym0 t) t :: Ordering) ~ Apply (Apply Compare_6989586621679389873Sym0 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_6989586621679389897Sym0 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_6989586621679389915Sym0 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_6989586621679389933Sym0 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_6989586621679389951Sym0 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_6989586621679389969Sym0 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_6989586621679389987Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a) Source #

#### Instances

Instances details

SOrd Bool Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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

Instance details

Defined in Data.Singletons.Prelude.Ord

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

Instance details

Defined in Data.Singletons.TypeLits.Internal

Methods

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

(%<) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #

(%<=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #

(%>) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #

(%>=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #

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

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

SOrd Symbol Source # |

Instance details

Defined in Data.Singletons.TypeLits.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 () Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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

Instance details

Defined in Data.Singletons.Prelude.Ord

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 Bool => SOrd All Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 a, SOrd [a]) => SOrd [a] Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (Maybe a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (NonEmpty a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (Down a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (Identity a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 a => SOrd (First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 (Maybe a) => SOrd (Option a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

sMin :: forall (t :: Option a) (t :: Option a). 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 :: 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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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.Singletons.Prelude.Semigroup.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 (Maybe a) => SOrd (First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monoid

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.Singletons.Prelude.Monoid

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 b) => SOrd (Either a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 a, SOrd b) => SOrd (a, b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (Arg a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup

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 c) => SOrd (a, b, c) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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 (Const a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Const

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 d) => SOrd (a, b, c, d) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

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.Singletons.Prelude.Ord

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.Singletons.Prelude.Ord

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.Singletons.Prelude.Ord

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

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.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.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SOrdering :: Ordering -> Type where Source #

Constructors

SLT :: SOrdering 'LT |
SEQ :: SOrdering 'EQ |
SGT :: SOrdering 'GT |

#### Instances

Instances details

TestCoercion SOrdering Source # |
Instance details Defined in Data.Singletons.Prelude.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.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (a :~: b)
Show (SOrdering z) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SOrdering z -> ShowS show :: SOrdering z -> String showList :: [SOrdering z] -> ShowS

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

Constructors

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

#### Instances

Instances details

SDecide a => TestCoercion (SDown :: Down a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord 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.Singletons.Prelude.Ord Methods testEquality :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (a0 :~: b)

## Defunctionalization symbols

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

#### Instances

Instances details

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 (a6989586621679400187 :: Ordering) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ThenCmpSym0 (a6989586621679400187 :: Ordering) = ThenCmpSym1 a6989586621679400187

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

#### Instances

Instances details

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 a6989586621679400187 :: TyFun Ordering Ordering -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ThenCmpSym1 a6989586621679400187 :: TyFun Ordering Ordering -> Type) (a6989586621679400188 :: Ordering) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ThenCmpSym1 a6989586621679400187 :: TyFun Ordering Ordering -> Type) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188

type ThenCmpSym2 (a6989586621679400187 :: Ordering) (a6989586621679400188 :: Ordering) = ThenCmp a6989586621679400187 a6989586621679400188 Source #

type LTSym0 = 'LT Source #

type EQSym0 = 'EQ Source #

type GTSym0 = 'GT Source #

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

#### Instances

Instances details

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 a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (CompareSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) (arg6989586621679389843 :: a6989586621679389754) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> Ordering) -> Type) (arg6989586621679389843 :: a6989586621679389754) = CompareSym1 arg6989586621679389843

data CompareSym1 (arg6989586621679389843 :: a6989586621679389754) :: (~>) a6989586621679389754 Ordering Source #

#### Instances

Instances details

(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 arg6989586621679389843 :: TyFun a6989586621679389754 Ordering -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (CompareSym1 arg6989586621679389843 :: TyFun a Ordering -> Type) (arg6989586621679389844 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (CompareSym1 arg6989586621679389843 :: TyFun a Ordering -> Type) (arg6989586621679389844 :: a) = Compare arg6989586621679389843 arg6989586621679389844

type CompareSym2 (arg6989586621679389843 :: a6989586621679389754) (arg6989586621679389844 :: a6989586621679389754) = Compare arg6989586621679389843 arg6989586621679389844 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

(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 ((<@#@$$) arg6989586621679389847 :: TyFun a6989586621679389754 Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((<@#@$$) arg6989586621679389847 :: TyFun a Bool -> Type) (arg6989586621679389848 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<@#@$$) arg6989586621679389847 :: TyFun a Bool -> Type) (arg6989586621679389848 :: a) = arg6989586621679389847 < arg6989586621679389848

type (<@#@$$$) (arg6989586621679389847 :: a6989586621679389754) (arg6989586621679389848 :: a6989586621679389754) = (<) arg6989586621679389847 arg6989586621679389848 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

(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 ((<=@#@$$) arg6989586621679389851 :: TyFun a6989586621679389754 Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((<=@#@$$) arg6989586621679389851 :: TyFun a Bool -> Type) (arg6989586621679389852 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((<=@#@$$) arg6989586621679389851 :: TyFun a Bool -> Type) (arg6989586621679389852 :: a) = arg6989586621679389851 <= arg6989586621679389852

type (<=@#@$$$) (arg6989586621679389851 :: a6989586621679389754) (arg6989586621679389852 :: a6989586621679389754) = (<=) arg6989586621679389851 arg6989586621679389852 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

(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 ((>@#@$$) arg6989586621679389855 :: TyFun a6989586621679389754 Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((>@#@$$) arg6989586621679389855 :: TyFun a Bool -> Type) (arg6989586621679389856 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>@#@$$) arg6989586621679389855 :: TyFun a Bool -> Type) (arg6989586621679389856 :: a) = arg6989586621679389855 > arg6989586621679389856

type (>@#@$$$) (arg6989586621679389855 :: a6989586621679389754) (arg6989586621679389856 :: a6989586621679389754) = (>) arg6989586621679389855 arg6989586621679389856 Source #

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

#### Instances

Instances details

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

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

#### Instances

Instances details

(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 ((>=@#@$$) arg6989586621679389859 :: TyFun a6989586621679389754 Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply ((>=@#@$$) arg6989586621679389859 :: TyFun a Bool -> Type) (arg6989586621679389860 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply ((>=@#@$$) arg6989586621679389859 :: TyFun a Bool -> Type) (arg6989586621679389860 :: a) = arg6989586621679389859 >= arg6989586621679389860

type (>=@#@$$$) (arg6989586621679389859 :: a6989586621679389754) (arg6989586621679389860 :: a6989586621679389754) = (>=) arg6989586621679389859 arg6989586621679389860 Source #

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

#### Instances

Instances details

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 a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MaxSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389863 :: a6989586621679389754) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MaxSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389863 :: a6989586621679389754) = MaxSym1 arg6989586621679389863

data MaxSym1 (arg6989586621679389863 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754 Source #

#### Instances

Instances details

(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 arg6989586621679389863 :: TyFun a6989586621679389754 a6989586621679389754 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MaxSym1 arg6989586621679389863 :: TyFun a a -> Type) (arg6989586621679389864 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MaxSym1 arg6989586621679389863 :: TyFun a a -> Type) (arg6989586621679389864 :: a) = Max arg6989586621679389863 arg6989586621679389864

type MaxSym2 (arg6989586621679389863 :: a6989586621679389754) (arg6989586621679389864 :: a6989586621679389754) = Max arg6989586621679389863 arg6989586621679389864 Source #

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

#### Instances

Instances details

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 a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MinSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389867 :: a6989586621679389754) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MinSym0 :: TyFun a6989586621679389754 (a6989586621679389754 ~> a6989586621679389754) -> Type) (arg6989586621679389867 :: a6989586621679389754) = MinSym1 arg6989586621679389867

data MinSym1 (arg6989586621679389867 :: a6989586621679389754) :: (~>) a6989586621679389754 a6989586621679389754 Source #

#### Instances

Instances details

(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 arg6989586621679389867 :: TyFun a6989586621679389754 a6989586621679389754 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (MinSym1 arg6989586621679389867 :: TyFun a a -> Type) (arg6989586621679389868 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (MinSym1 arg6989586621679389867 :: TyFun a a -> Type) (arg6989586621679389868 :: a) = Min arg6989586621679389867 arg6989586621679389868

type MinSym2 (arg6989586621679389867 :: a6989586621679389754) (arg6989586621679389868 :: a6989586621679389754) = Min arg6989586621679389867 arg6989586621679389868 Source #

data ComparingSym0 :: forall b6989586621679389744 a6989586621679389743. (~>) ((~>) b6989586621679389744 a6989586621679389743) ((~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering)) Source #

#### Instances

Instances details

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 (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ComparingSym0 :: TyFun (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) (a6989586621679389834 :: b6989586621679389744 ~> a6989586621679389743) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym0 :: TyFun (b6989586621679389744 ~> a6989586621679389743) (b6989586621679389744 ~> (b6989586621679389744 ~> Ordering)) -> Type) (a6989586621679389834 :: b6989586621679389744 ~> a6989586621679389743) = ComparingSym1 a6989586621679389834

data ComparingSym1 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) :: (~>) b6989586621679389744 ((~>) b6989586621679389744 Ordering) Source #

#### Instances

Instances details

(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 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ComparingSym1 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) (a6989586621679389835 :: b6989586621679389744) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym1 a6989586621679389834 :: TyFun b6989586621679389744 (b6989586621679389744 ~> Ordering) -> Type) (a6989586621679389835 :: b6989586621679389744) = ComparingSym2 a6989586621679389834 a6989586621679389835

data ComparingSym2 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) :: (~>) b6989586621679389744 Ordering Source #

#### Instances

Instances details

(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 a6989586621679389835 a6989586621679389834 :: TyFun b6989586621679389744 Ordering -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods suppressUnusedWarnings :: () Source #
type Apply (ComparingSym2 a6989586621679389835 a6989586621679389834 :: TyFun b Ordering -> Type) (a6989586621679389836 :: b) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Apply (ComparingSym2 a6989586621679389835 a6989586621679389834 :: TyFun b Ordering -> Type) (a6989586621679389836 :: b) = Comparing a6989586621679389835 a6989586621679389834 a6989586621679389836

type ComparingSym3 (a6989586621679389834 :: (~>) b6989586621679389744 a6989586621679389743) (a6989586621679389835 :: b6989586621679389744) (a6989586621679389836 :: b6989586621679389744) = Comparing a6989586621679389834 a6989586621679389835 a6989586621679389836 Source #

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

#### Instances

Instances details

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

type DownSym1 (t6989586621679398850 :: a6989586621679089884) = 'Down t6989586621679398850 Source #

# Orphan instances

SingKind a => SingKind (Down a) Source # |
Instance details Associated Types type Demote (Down a) = (r :: Type) Source # Methods fromSing :: forall (a0 :: Down a). Sing a0 -> Demote (Down a) Source # toSing :: Demote (Down a) -> SomeSing (Down a) Source #
SDecide a => SDecide (Down a) Source # |
Instance details Methods (%~) :: forall (a0 :: Down a) (b :: Down a). 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 (%==) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Sing (a0 == b) Source # (%/=) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Sing (a0 /= b) Source #
SingI n => SingI ('Down n :: Down a) Source # |
Instance details Methods sing :: Sing ('Down n) Source #