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

Data.Ord.Singletons

Contents

Defunctionalization symbols
Orphan instances

Description

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

Synopsis

class POrd a where
- type Compare (arg :: a) (arg1 :: a) :: Ordering
- type (arg :: a) < (arg1 :: a) :: Bool
- type (arg :: a) <= (arg1 :: a) :: Bool
- type (arg :: a) > (arg1 :: a) :: Bool
- type (arg :: a) >= (arg1 :: a) :: Bool
- type Max (arg :: a) (arg1 :: a) :: a
- type Min (arg :: a) (arg1 :: a) :: a
class SEq a => SOrd a where
- sCompare :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Compare t1 t2)
- (%<) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 < t2)
- (%<=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 <= t2)
- (%>) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 > t2)
- (%>=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 >= t2)
- sMax :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Max t1 t2)
- sMin :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Min t1 t2)
type family Comparing (a1 :: b ~> a) (a2 :: b) (a3 :: b) :: Ordering where ...
sComparing :: forall b a (t1 :: b ~> a) (t2 :: b) (t3 :: b). SOrd a => Sing t1 -> Sing t2 -> Sing t3 -> Sing (Comparing t1 t2 t3)
type family Sing :: k -> Type
data SOrdering (a :: Ordering) where
- SLT :: SOrdering 'LT
- SEQ :: SOrdering 'EQ
- SGT :: SOrdering 'GT
data SDown (a1 :: Down a) where
- SDown :: forall a (n :: a). Sing n -> SDown ('Down n)
type family GetDown (a1 :: Down a) :: a where ...
sGetDown :: forall a (t :: Down a). Sing t -> Sing (GetDown t)
type family LTSym0 :: Ordering where ...
type family EQSym0 :: Ordering where ...
type family GTSym0 :: Ordering where ...
data CompareSym0 (a1 :: TyFun a (a ~> Ordering))
data CompareSym1 (a6989586621679189966 :: a) (b :: TyFun a Ordering)
type family CompareSym2 (a6989586621679189966 :: a) (a6989586621679189967 :: a) :: Ordering where ...
data (<@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679189971 :: a) <@#@$$ (b :: TyFun a Bool)
type family (a6989586621679189971 :: a) <@#@$$$ (a6989586621679189972 :: a) :: Bool where ...
data (<=@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679189976 :: a) <=@#@$$ (b :: TyFun a Bool)
type family (a6989586621679189976 :: a) <=@#@$$$ (a6989586621679189977 :: a) :: Bool where ...
data (>@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679189981 :: a) >@#@$$ (b :: TyFun a Bool)
type family (a6989586621679189981 :: a) >@#@$$$ (a6989586621679189982 :: a) :: Bool where ...
data (>=@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679189986 :: a) >=@#@$$ (b :: TyFun a Bool)
type family (a6989586621679189986 :: a) >=@#@$$$ (a6989586621679189987 :: a) :: Bool where ...
data MaxSym0 (a1 :: TyFun a (a ~> a))
data MaxSym1 (a6989586621679189991 :: a) (b :: TyFun a a)
type family MaxSym2 (a6989586621679189991 :: a) (a6989586621679189992 :: a) :: a where ...
data MinSym0 (a1 :: TyFun a (a ~> a))
data MinSym1 (a6989586621679189996 :: a) (b :: TyFun a a)
type family MinSym2 (a6989586621679189996 :: a) (a6989586621679189997 :: a) :: a where ...
data ComparingSym0 (a1 :: TyFun (b ~> a) (b ~> (b ~> Ordering)))
data ComparingSym1 (a6989586621679189957 :: b ~> a) (b1 :: TyFun b (b ~> Ordering))
data ComparingSym2 (a6989586621679189957 :: b ~> a) (a6989586621679189958 :: b) (c :: TyFun b Ordering)
type family ComparingSym3 (a6989586621679189957 :: b ~> a) (a6989586621679189958 :: b) (a6989586621679189959 :: b) :: Ordering where ...
data DownSym0 (a1 :: TyFun a (Down a))
type family DownSym1 (a6989586621679198735 :: a) :: Down a where ...
data GetDownSym0 (a1 :: TyFun (Down a) a)
type family GetDownSym1 (a6989586621679198738 :: Down a) :: a where ...

Documentation

class POrd a Source #

Associated Types

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

type Compare (arg :: a) (arg1 :: a) = Compare_6989586621679190000 arg arg1

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

type (arg :: a) < (arg1 :: a) = TFHelper_6989586621679190021 arg arg1

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

type (arg :: a) <= (arg1 :: a) = TFHelper_6989586621679190037 arg arg1

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

type (arg :: a) > (arg1 :: a) = TFHelper_6989586621679190053 arg arg1

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

type (arg :: a) >= (arg1 :: a) = TFHelper_6989586621679190069 arg arg1

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

type Max (arg :: a) (arg1 :: a) = Max_6989586621679190085 arg arg1

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

type Min (arg :: a) (arg1 :: a) = Min_6989586621679190101 arg arg1

Instances

Instances details

POrd Void Source #

Instance details

Defined in Data.Ord.Singletons

Associated Types

type Compare (a1 :: Void) (a2 :: Void)
Instance details Defined in Data.Ord.Singletons type Compare (a1 :: Void) (a2 :: Void)
type (arg1 :: Void) < (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Void) < (arg2 :: Void)
type (arg1 :: Void) <= (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Void) <= (arg2 :: Void)
type (arg1 :: Void) > (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Void) > (arg2 :: Void)
type (arg1 :: Void) >= (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Void) >= (arg2 :: Void)
type Max (arg1 :: Void) (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type Max (arg1 :: Void) (arg2 :: Void)
type Min (arg1 :: Void) (arg2 :: Void)
Instance details Defined in Data.Ord.Singletons type Min (arg1 :: Void) (arg2 :: Void)

POrd All Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type Compare (a1 :: All) (a2 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Compare (a1 :: All) (a2 :: All)
type (arg :: All) < (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: All) < (arg1 :: All)
type (arg :: All) <= (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: All) <= (arg1 :: All)
type (arg :: All) > (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: All) > (arg1 :: All)
type (arg :: All) >= (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: All) >= (arg1 :: All)
type Max (arg :: All) (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Max (arg :: All) (arg1 :: All)
type Min (arg :: All) (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Min (arg :: All) (arg1 :: All)

POrd Any Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type Compare (a1 :: Any) (a2 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Compare (a1 :: Any) (a2 :: Any)
type (arg :: Any) < (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: Any) < (arg1 :: Any)
type (arg :: Any) <= (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: Any) <= (arg1 :: Any)
type (arg :: Any) > (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: Any) > (arg1 :: Any)
type (arg :: Any) >= (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: Any) >= (arg1 :: Any)
type Max (arg :: Any) (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Max (arg :: Any) (arg1 :: Any)
type Min (arg :: Any) (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type Min (arg :: Any) (arg1 :: Any)

POrd Ordering Source #

Instance details

Defined in Data.Ord.Singletons

Associated Types

type Compare (a1 :: Ordering) (a2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type Compare (a1 :: Ordering) (a2 :: Ordering)
type (arg1 :: Ordering) < (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Ordering) < (arg2 :: Ordering)
type (arg1 :: Ordering) <= (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Ordering) <= (arg2 :: Ordering)
type (arg1 :: Ordering) > (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Ordering) > (arg2 :: Ordering)
type (arg1 :: Ordering) >= (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Ordering) >= (arg2 :: Ordering)
type Max (arg1 :: Ordering) (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type Max (arg1 :: Ordering) (arg2 :: Ordering)
type Min (arg1 :: Ordering) (arg2 :: Ordering)
Instance details Defined in Data.Ord.Singletons type Min (arg1 :: Ordering) (arg2 :: Ordering)

POrd Natural Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare (a :: Natural) (b :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Compare (a :: Natural) (b :: Natural) = CmpNat a b
type (arg :: Natural) < (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Natural) < (arg1 :: Natural)
type (arg :: Natural) <= (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Natural) <= (arg1 :: Natural)
type (arg :: Natural) > (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Natural) > (arg1 :: Natural)
type (arg :: Natural) >= (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Natural) >= (arg1 :: Natural)
type Max (arg :: Natural) (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Max (arg :: Natural) (arg1 :: Natural)
type Min (arg :: Natural) (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Min (arg :: Natural) (arg1 :: Natural)

POrd () Source #

Instance details

Defined in Data.Ord.Singletons

Associated Types

type Compare (a1 :: ()) (a2 :: ())
Instance details Defined in Data.Ord.Singletons type Compare (a1 :: ()) (a2 :: ())
type (arg1 :: ()) < (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type (arg1 :: ()) < (arg2 :: ())
type (arg1 :: ()) <= (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type (arg1 :: ()) <= (arg2 :: ())
type (arg1 :: ()) > (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type (arg1 :: ()) > (arg2 :: ())
type (arg1 :: ()) >= (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type (arg1 :: ()) >= (arg2 :: ())
type Max (arg1 :: ()) (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type Max (arg1 :: ()) (arg2 :: ())
type Min (arg1 :: ()) (arg2 :: ())
Instance details Defined in Data.Ord.Singletons type Min (arg1 :: ()) (arg2 :: ())

POrd Bool Source #

Instance details

Defined in Data.Ord.Singletons

Associated Types

type Compare (a1 :: Bool) (a2 :: Bool)
Instance details Defined in Data.Ord.Singletons type Compare (a1 :: Bool) (a2 :: Bool)
type (arg1 :: Bool) < (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Bool) < (arg2 :: Bool)
type (arg1 :: Bool) <= (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Bool) <= (arg2 :: Bool)
type (arg1 :: Bool) > (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Bool) > (arg2 :: Bool)
type (arg1 :: Bool) >= (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type (arg1 :: Bool) >= (arg2 :: Bool)
type Max (arg1 :: Bool) (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type Max (arg1 :: Bool) (arg2 :: Bool)
type Min (arg1 :: Bool) (arg2 :: Bool)
Instance details Defined in Data.Ord.Singletons type Min (arg1 :: Bool) (arg2 :: Bool)

POrd Char Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare (a :: Char) (b :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Compare (a :: Char) (b :: Char) = CmpChar a b
type (arg :: Char) < (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Char) < (arg1 :: Char)
type (arg :: Char) <= (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Char) <= (arg1 :: Char)
type (arg :: Char) > (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Char) > (arg1 :: Char)
type (arg :: Char) >= (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Char) >= (arg1 :: Char)
type Max (arg :: Char) (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Max (arg :: Char) (arg1 :: Char)
type Min (arg :: Char) (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Min (arg :: Char) (arg1 :: Char)

POrd Symbol Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare (a :: Symbol) (b :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b
type (arg :: Symbol) < (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Symbol) < (arg1 :: Symbol)
type (arg :: Symbol) <= (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Symbol) <= (arg1 :: Symbol)
type (arg :: Symbol) > (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Symbol) > (arg1 :: Symbol)
type (arg :: Symbol) >= (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Symbol) >= (arg1 :: Symbol)
type Max (arg :: Symbol) (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Max (arg :: Symbol) (arg1 :: Symbol)
type Min (arg :: Symbol) (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type Min (arg :: Symbol) (arg1 :: Symbol)

POrd (First a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Last a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Max a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Min a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (WrappedMonoid m) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (NonEmpty a) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Identity a) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (First a) Source #

Instance details

Defined in Data.Monoid.Singletons

POrd (Last a) Source #

Instance details

Defined in Data.Monoid.Singletons

POrd (Down a) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Dual a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Product a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Sum a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

POrd (Maybe a) Source #

Instance details

Defined in Data.Ord.Singletons

POrd [a] Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Arg a b) Source #

Instance details

Defined in Data.Semigroup.Singletons

POrd (Either a b) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Proxy s) Source #

Instance details

Defined in Data.Proxy.Singletons

POrd (a, b) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Const a b) Source #

Instance details

Defined in Data.Functor.Const.Singletons

POrd (a, b, c) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Product f g a) Source #

Instance details

Defined in Data.Functor.Product.Singletons

POrd (Sum f g a) Source #

Instance details

Defined in Data.Functor.Sum.Singletons

POrd (a, b, c, d) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (Compose f g a) Source #

Instance details

Defined in Data.Functor.Compose.Singletons

POrd (a, b, c, d, e) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (a, b, c, d, e, f) Source #

Instance details

Defined in Data.Ord.Singletons

POrd (a, b, c, d, e, f, g) Source #

Instance details

Defined in Data.Ord.Singletons

class SEq a => SOrd a where Source #

Minimal complete definition

Nothing

Methods

sCompare :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Compare t1 t2) Source #

default sCompare :: forall (t1 :: a) (t2 :: a). Compare t1 t2 ~ Compare_6989586621679190000 t1 t2 => Sing t1 -> Sing t2 -> Sing (Compare t1 t2) Source #

(%<) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 < t2) infix 4 Source #

default (%<) :: forall (t1 :: a) (t2 :: a). (t1 < t2) ~ TFHelper_6989586621679190021 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 < t2) Source #

(%<=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 <= t2) infix 4 Source #

default (%<=) :: forall (t1 :: a) (t2 :: a). (t1 <= t2) ~ TFHelper_6989586621679190037 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 <= t2) Source #

(%>) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 > t2) infix 4 Source #

default (%>) :: forall (t1 :: a) (t2 :: a). (t1 > t2) ~ TFHelper_6989586621679190053 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 > t2) Source #

(%>=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 >= t2) infix 4 Source #

default (%>=) :: forall (t1 :: a) (t2 :: a). (t1 >= t2) ~ TFHelper_6989586621679190069 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 >= t2) Source #

sMax :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Max t1 t2) Source #

default sMax :: forall (t1 :: a) (t2 :: a). Max t1 t2 ~ Max_6989586621679190085 t1 t2 => Sing t1 -> Sing t2 -> Sing (Max t1 t2) Source #

sMin :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Min t1 t2) Source #

default sMin :: forall (t1 :: a) (t2 :: a). Min t1 t2 ~ Min_6989586621679190101 t1 t2 => Sing t1 -> Sing t2 -> Sing (Min t1 t2) Source #

Instances

Instances details

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

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

Equations

Comparing (p :: k1 ~> k2) (x :: k1) (y :: k1) = Apply (Apply (CompareSym0 :: TyFun k2 (k2 ~> Ordering) -> Type) (Apply p x)) (Apply p y)

sComparing :: forall b a (t1 :: b ~> a) (t2 :: b) (t3 :: b). SOrd a => Sing t1 -> Sing t2 -> Sing t3 -> Sing (Comparing t1 t2 t3) Source #

type family Sing :: k -> Type #

Instances

Instances details

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

data SOrdering (a :: Ordering) where Source #

Constructors

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

Instances

Instances details

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

data SDown (a1 :: Down a) where Source #

Constructors

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

Instances

Instances details

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

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

Equations

GetDown ('Down field :: Down a) = field

sGetDown :: forall a (t :: Down a). Sing t -> Sing (GetDown t) Source #

Defunctionalization symbols

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

Equations

LTSym0 = 'LT

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

Equations

EQSym0 = 'EQ

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

Equations

GTSym0 = 'GT

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

Instances

Instances details

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

data CompareSym1 (a6989586621679189966 :: a) (b :: TyFun a Ordering) Source #

Instances

Instances details

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

type family CompareSym2 (a6989586621679189966 :: a) (a6989586621679189967 :: a) :: Ordering where ... Source #

Equations

CompareSym2 (a6989586621679189966 :: a) (a6989586621679189967 :: a) = Compare a6989586621679189966 a6989586621679189967

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

Instances

Instances details

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

data (a6989586621679189971 :: a) <@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

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

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

Equations

(a6989586621679189971 :: a) <@#@$$$ (a6989586621679189972 :: a) = a6989586621679189971 < a6989586621679189972

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

Instances

Instances details

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

data (a6989586621679189976 :: a) <=@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

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

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

Equations

(a6989586621679189976 :: a) <=@#@$$$ (a6989586621679189977 :: a) = a6989586621679189976 <= a6989586621679189977

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

Instances

Instances details

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

data (a6989586621679189981 :: a) >@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

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

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

Equations

(a6989586621679189981 :: a) >@#@$$$ (a6989586621679189982 :: a) = a6989586621679189981 > a6989586621679189982

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

Instances

Instances details

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

data (a6989586621679189986 :: a) >=@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

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

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

Equations

(a6989586621679189986 :: a) >=@#@$$$ (a6989586621679189987 :: a) = a6989586621679189986 >= a6989586621679189987

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

Instances

Instances details

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

data MaxSym1 (a6989586621679189991 :: a) (b :: TyFun a a) Source #

Instances

Instances details

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

type family MaxSym2 (a6989586621679189991 :: a) (a6989586621679189992 :: a) :: a where ... Source #

Equations

MaxSym2 (a6989586621679189991 :: a) (a6989586621679189992 :: a) = Max a6989586621679189991 a6989586621679189992

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

Instances

Instances details

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

data MinSym1 (a6989586621679189996 :: a) (b :: TyFun a a) Source #

Instances

Instances details

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

type family MinSym2 (a6989586621679189996 :: a) (a6989586621679189997 :: a) :: a where ... Source #

Equations

MinSym2 (a6989586621679189996 :: a) (a6989586621679189997 :: a) = Min a6989586621679189996 a6989586621679189997

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

Instances

Instances details

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

data ComparingSym1 (a6989586621679189957 :: b ~> a) (b1 :: TyFun b (b ~> Ordering)) Source #

Instances

Instances details

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

data ComparingSym2 (a6989586621679189957 :: b ~> a) (a6989586621679189958 :: b) (c :: TyFun b Ordering) Source #

Instances

Instances details

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

type family ComparingSym3 (a6989586621679189957 :: b ~> a) (a6989586621679189958 :: b) (a6989586621679189959 :: b) :: Ordering where ... Source #

Equations

ComparingSym3 (a6989586621679189957 :: b ~> a) (a6989586621679189958 :: b) (a6989586621679189959 :: b) = Comparing a6989586621679189957 a6989586621679189958 a6989586621679189959

data DownSym0 (a1 :: TyFun a (Down a)) Source #

Instances

Instances details

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

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

Equations

DownSym1 (a6989586621679198735 :: a) = 'Down a6989586621679198735

data GetDownSym0 (a1 :: TyFun (Down a) a) Source #

Instances

Instances details

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

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

Equations

GetDownSym1 (a6989586621679198738 :: Down a) = GetDown a6989586621679198738

Orphan instances

SingI1 ('Down :: k1 -> Down k1) Source #

Instance details

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('Down x) #

SingKind a => SingKind (Down a) Source #

Instance details

Associated Types

type Demote (Down a)
Instance details Defined in Data.Ord.Singletons type Demote (Down a) = Down (Demote a)

Methods

fromSing :: forall (a0 :: Down a). Sing a0 -> Demote (Down a) #

toSing :: Demote (Down a) -> SomeSing (Down a) #

SDecide a => SDecide (Down a) Source #

Instance details

Methods

(%~) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Decision (a0 :~: b) #

PEq (Down a) Source #

Instance details

SEq a => SEq (Down a) Source #

Instance details

Methods

(%==) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source #

(%/=) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #

PSemigroup (Down a) Source #

Instance details

SSemigroup a => SSemigroup (Down a) Source #

Instance details

Methods

(%<>) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (t1 <> t2) Source #

sSconcat :: forall (t :: NonEmpty (Down a)). Sing t -> Sing (Sconcat t) Source #

SingI n => SingI ('Down n :: Down a) Source #

Instance details

Methods

sing :: Sing ('Down n) #