singletons-2.6: A framework for generating singleton types
Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Ord

Description

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

Synopsis

Documentation

class POrd (a :: Type) Source #

Associated Types

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

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

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

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

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

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

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

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

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

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

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

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

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

type Min a a = Apply (Apply Min_6989586621679394171Sym0 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 (Min a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Max a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (WrappedMonoid m) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Option a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Identity a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (First a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Last a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Dual a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Sum a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Product a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Down a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (NonEmpty a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Either a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Arg a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (a, b, c) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

POrd (Const a b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Const

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering Source #

type arg < arg :: Bool Source #

type arg <= arg :: Bool Source #

type arg > arg :: Bool Source #

type arg >= arg :: Bool Source #

type Max arg arg :: a Source #

type Min arg arg :: a Source #

class SEq a => SOrd a where Source #

Minimal complete definition

Nothing

Methods

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

default sCompare :: forall (t :: a) (t :: a). (Apply (Apply CompareSym0 t) t :: Ordering) ~ Apply (Apply Compare_6989586621679394057Sym0 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_6989586621679394081Sym0 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_6989586621679394099Sym0 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_6989586621679394117Sym0 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_6989586621679394135Sym0 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_6989586621679394153Sym0 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_6989586621679394171Sym0 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 (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 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 (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 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 (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 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 (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 (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 (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 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 (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 [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 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.

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 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 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 TypeReps (for instance, TypeReps 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.Semigroup.Internal

type Sing = SMin :: Min 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 = 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 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.Instances

type Sing = SIdentity :: Identity 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.Semigroup.Internal

type Sing = SDual :: Dual 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.Semigroup.Internal

type Sing = SProduct :: Product 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 = SNonEmpty :: NonEmpty 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.Prelude.Semigroup

type Sing = SArg :: Arg 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 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) Source # 
Instance details

Defined in Data.Singletons.ShowSing

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

SuppressUnusedWarnings ThenCmpSym0 Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ThenCmpSym0 (a6989586621679404371 :: Ordering) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ThenCmpSym0 (a6989586621679404371 :: Ordering) = ThenCmpSym1 a6989586621679404371

data ThenCmpSym1 (a6989586621679404371 :: 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 a6989586621679404371 :: TyFun Ordering Ordering -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ThenCmpSym1 a6989586621679404371 :: TyFun Ordering Ordering -> Type) (a6989586621679404372 :: Ordering) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ThenCmpSym1 a6989586621679404371 :: TyFun Ordering Ordering -> Type) (a6989586621679404372 :: Ordering) = ThenCmp a6989586621679404371 a6989586621679404372

type ThenCmpSym2 (a6989586621679404371 :: Ordering) (a6989586621679404372 :: Ordering) = ThenCmp a6989586621679404371 a6989586621679404372 Source #

type LTSym0 = 'LT Source #

type EQSym0 = 'EQ Source #

type GTSym0 = 'GT Source #

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

Instances

Instances details
SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> Ordering) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> Ordering) -> Type) (arg6989586621679394027 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> Ordering) -> Type) (arg6989586621679394027 :: a6989586621679393938) = CompareSym1 arg6989586621679394027

data CompareSym1 (arg6989586621679394027 :: a6989586621679393938) :: (~>) a6989586621679393938 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 arg6989586621679394027 :: TyFun a6989586621679393938 Ordering -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 arg6989586621679394027 :: TyFun a Ordering -> Type) (arg6989586621679394028 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 arg6989586621679394027 :: TyFun a Ordering -> Type) (arg6989586621679394028 :: a) = Compare arg6989586621679394027 arg6989586621679394028

type CompareSym2 (arg6989586621679394027 :: a6989586621679393938) (arg6989586621679394028 :: a6989586621679393938) = Compare arg6989586621679394027 arg6989586621679394028 Source #

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

Instances

Instances details
SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394031 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394031 :: a6989586621679393938) = (<@#@$$) arg6989586621679394031

data (<@#@$$) (arg6989586621679394031 :: a6989586621679393938) :: (~>) a6989586621679393938 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 ((<@#@$$) arg6989586621679394031 :: TyFun a6989586621679393938 Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$$) arg6989586621679394031 :: TyFun a Bool -> Type) (arg6989586621679394032 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$$) arg6989586621679394031 :: TyFun a Bool -> Type) (arg6989586621679394032 :: a) = arg6989586621679394031 < arg6989586621679394032

type (<@#@$$$) (arg6989586621679394031 :: a6989586621679393938) (arg6989586621679394032 :: a6989586621679393938) = (<) arg6989586621679394031 arg6989586621679394032 Source #

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

Instances

Instances details
SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394035 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394035 :: a6989586621679393938) = (<=@#@$$) arg6989586621679394035

data (<=@#@$$) (arg6989586621679394035 :: a6989586621679393938) :: (~>) a6989586621679393938 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 ((<=@#@$$) arg6989586621679394035 :: TyFun a6989586621679393938 Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$$) arg6989586621679394035 :: TyFun a Bool -> Type) (arg6989586621679394036 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$$) arg6989586621679394035 :: TyFun a Bool -> Type) (arg6989586621679394036 :: a) = arg6989586621679394035 <= arg6989586621679394036

type (<=@#@$$$) (arg6989586621679394035 :: a6989586621679393938) (arg6989586621679394036 :: a6989586621679393938) = (<=) arg6989586621679394035 arg6989586621679394036 Source #

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

Instances

Instances details
SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394039 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394039 :: a6989586621679393938) = (>@#@$$) arg6989586621679394039

data (>@#@$$) (arg6989586621679394039 :: a6989586621679393938) :: (~>) a6989586621679393938 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 ((>@#@$$) arg6989586621679394039 :: TyFun a6989586621679393938 Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) arg6989586621679394039 :: TyFun a Bool -> Type) (arg6989586621679394040 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) arg6989586621679394039 :: TyFun a Bool -> Type) (arg6989586621679394040 :: a) = arg6989586621679394039 > arg6989586621679394040

type (>@#@$$$) (arg6989586621679394039 :: a6989586621679393938) (arg6989586621679394040 :: a6989586621679393938) = (>) arg6989586621679394039 arg6989586621679394040 Source #

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

Instances

Instances details
SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394043 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a6989586621679393938 (a6989586621679393938 ~> Bool) -> Type) (arg6989586621679394043 :: a6989586621679393938) = (>=@#@$$) arg6989586621679394043

data (>=@#@$$) (arg6989586621679394043 :: a6989586621679393938) :: (~>) a6989586621679393938 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 ((>=@#@$$) arg6989586621679394043 :: TyFun a6989586621679393938 Bool -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) arg6989586621679394043 :: TyFun a Bool -> Type) (arg6989586621679394044 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) arg6989586621679394043 :: TyFun a Bool -> Type) (arg6989586621679394044 :: a) = arg6989586621679394043 >= arg6989586621679394044

type (>=@#@$$$) (arg6989586621679394043 :: a6989586621679393938) (arg6989586621679394044 :: a6989586621679393938) = (>=) arg6989586621679394043 arg6989586621679394044 Source #

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

Instances

Instances details
SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) (arg6989586621679394047 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) (arg6989586621679394047 :: a6989586621679393938) = MaxSym1 arg6989586621679394047

data MaxSym1 (arg6989586621679394047 :: a6989586621679393938) :: (~>) a6989586621679393938 a6989586621679393938 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 arg6989586621679394047 :: TyFun a6989586621679393938 a6989586621679393938 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 arg6989586621679394047 :: TyFun a a -> Type) (arg6989586621679394048 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 arg6989586621679394047 :: TyFun a a -> Type) (arg6989586621679394048 :: a) = Max arg6989586621679394047 arg6989586621679394048

type MaxSym2 (arg6989586621679394047 :: a6989586621679393938) (arg6989586621679394048 :: a6989586621679393938) = Max arg6989586621679394047 arg6989586621679394048 Source #

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

Instances

Instances details
SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) (arg6989586621679394051 :: a6989586621679393938) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679393938 (a6989586621679393938 ~> a6989586621679393938) -> Type) (arg6989586621679394051 :: a6989586621679393938) = MinSym1 arg6989586621679394051

data MinSym1 (arg6989586621679394051 :: a6989586621679393938) :: (~>) a6989586621679393938 a6989586621679393938 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 arg6989586621679394051 :: TyFun a6989586621679393938 a6989586621679393938 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 arg6989586621679394051 :: TyFun a a -> Type) (arg6989586621679394052 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 arg6989586621679394051 :: TyFun a a -> Type) (arg6989586621679394052 :: a) = Min arg6989586621679394051 arg6989586621679394052

type MinSym2 (arg6989586621679394051 :: a6989586621679393938) (arg6989586621679394052 :: a6989586621679393938) = Min arg6989586621679394051 arg6989586621679394052 Source #

data ComparingSym0 :: forall b6989586621679393928 a6989586621679393927. (~>) ((~>) b6989586621679393928 a6989586621679393927) ((~>) b6989586621679393928 ((~>) b6989586621679393928 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

SuppressUnusedWarnings (ComparingSym0 :: TyFun (b6989586621679393928 ~> a6989586621679393927) (b6989586621679393928 ~> (b6989586621679393928 ~> Ordering)) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym0 :: TyFun (b6989586621679393928 ~> a6989586621679393927) (b6989586621679393928 ~> (b6989586621679393928 ~> Ordering)) -> Type) (a6989586621679394018 :: b6989586621679393928 ~> a6989586621679393927) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym0 :: TyFun (b6989586621679393928 ~> a6989586621679393927) (b6989586621679393928 ~> (b6989586621679393928 ~> Ordering)) -> Type) (a6989586621679394018 :: b6989586621679393928 ~> a6989586621679393927) = ComparingSym1 a6989586621679394018

data ComparingSym1 (a6989586621679394018 :: (~>) b6989586621679393928 a6989586621679393927) :: (~>) b6989586621679393928 ((~>) b6989586621679393928 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

SuppressUnusedWarnings (ComparingSym1 a6989586621679394018 :: TyFun b6989586621679393928 (b6989586621679393928 ~> Ordering) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym1 a6989586621679394018 :: TyFun b6989586621679393928 (b6989586621679393928 ~> Ordering) -> Type) (a6989586621679394019 :: b6989586621679393928) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym1 a6989586621679394018 :: TyFun b6989586621679393928 (b6989586621679393928 ~> Ordering) -> Type) (a6989586621679394019 :: b6989586621679393928) = ComparingSym2 a6989586621679394018 a6989586621679394019

data ComparingSym2 (a6989586621679394018 :: (~>) b6989586621679393928 a6989586621679393927) (a6989586621679394019 :: b6989586621679393928) :: (~>) b6989586621679393928 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 a6989586621679394019 a6989586621679394018 :: TyFun b6989586621679393928 Ordering -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym2 a6989586621679394019 a6989586621679394018 :: TyFun b Ordering -> Type) (a6989586621679394020 :: b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym2 a6989586621679394019 a6989586621679394018 :: TyFun b Ordering -> Type) (a6989586621679394020 :: b) = Comparing a6989586621679394019 a6989586621679394018 a6989586621679394020

type ComparingSym3 (a6989586621679394018 :: (~>) b6989586621679393928 a6989586621679393927) (a6989586621679394019 :: b6989586621679393928) (a6989586621679394020 :: b6989586621679393928) = Comparing a6989586621679394018 a6989586621679394019 a6989586621679394020 Source #

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

Instances

Instances details
SingI (DownSym0 :: TyFun a (Down a) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

SuppressUnusedWarnings (DownSym0 :: TyFun a6989586621679097355 (Down a6989586621679097355) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (DownSym0 :: TyFun a (Down a) -> Type) (t6989586621679403034 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Ord

type Apply (DownSym0 :: TyFun a (Down a) -> Type) (t6989586621679403034 :: a) = 'Down t6989586621679403034

type DownSym1 (t6989586621679403034 :: a6989586621679097355) = 'Down t6989586621679403034 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 ('Down0 n) Source #