Data.Singletons.Prelude.Ord

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

Documentation

class POrd a

Associated Types

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

type Compare a a = Apply (Apply Compare_6989586621679383674Sym0 a) a

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

type a < a = Apply (Apply TFHelper_6989586621679383695Sym0 a) a

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

type a <= a = Apply (Apply TFHelper_6989586621679383711Sym0 a) a

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

type a > a = Apply (Apply TFHelper_6989586621679383727Sym0 a) a

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

type a >= a = Apply (Apply TFHelper_6989586621679383743Sym0 a) a

type Max (arg :: a) (arg :: a) :: a

type Max a a = Apply (Apply Max_6989586621679383759Sym0 a) a

type Min (arg :: a) (arg :: a) :: a

type Min a a = Apply (Apply Min_6989586621679383775Sym0 a) a

Instances

POrd Bool

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd Ordering

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd Nat

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd Symbol

Defined in Data.Singletons.TypeLits.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd ()

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd Void

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd All

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd Any

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd [a]

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Maybe a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Identity a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (First a)

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Last a)

Defined in Data.Singletons.Prelude.Monoid

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Down a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Either a b)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (a, b)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Proxy s)

Defined in Data.Singletons.Prelude.Proxy

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (a, b, c)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (Const a b)

Defined in Data.Singletons.Prelude.Const

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

POrd (a, b, c, d)

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

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

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

class SEq a => SOrd a where

Minimal complete definition

Nothing

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instances

SOrd Bool

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

sMax :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd Ordering

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

sMax :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

SOrd Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

sCompare :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

sMax :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd ()

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd Void

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

sMax :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd Bool => SOrd All

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

sMax :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd Bool => SOrd Any

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

sCompare :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

sMax :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd [a]) => SOrd [a]

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

(%>) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

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

sMax :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd a => SOrd (Maybe a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Min a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Max a)

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)

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

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

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

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

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

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

SOrd a => SOrd (First a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Last a)

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)

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

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

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

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

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

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

SOrd m => SOrd (WrappedMonoid m)

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)

(%<) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

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

(%>) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

sMax :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd (Maybe a) => SOrd (Option a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Identity a)

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)

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

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

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

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

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

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

SOrd (Maybe a) => SOrd (First a)

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)

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

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

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

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

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

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

SOrd (Maybe a) => SOrd (Last a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Dual a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Sum a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Product a)

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)

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

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

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

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

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

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

SOrd a => SOrd (Down a)

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)

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

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

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

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

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

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

(SOrd a, SOrd [a]) => SOrd (NonEmpty a)

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)

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

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

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

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

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

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

(SOrd a, SOrd b) => SOrd (Either a b)

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)

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

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

(%>) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

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

sMax :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd b) => SOrd (a, b)

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)

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

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

(%>) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

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

sMax :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd a => SOrd (Arg a b)

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)

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

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

(%>) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

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

sMax :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd (Proxy s)

Defined in Data.Singletons.Prelude.Proxy

Methods

sCompare :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

(%<) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

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

(%>) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

sMax :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd b, SOrd c) => SOrd (a, b, c)

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)

(%<) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

(%<=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)

(%>) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

sMax :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

SOrd a => SOrd (Const a b)

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)

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

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

(%>) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

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

sMax :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (a, b, c, d)

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)

(%<) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

(%<=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)

(%>) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

sMax :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) => SOrd (a, b, c, d, e)

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)

(%<) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

(%<=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)

(%>) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

sMax :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) => SOrd (a, b, c, d, e, f)

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)

(%<) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

(%<=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)

(%>) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t)

(%>=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t)

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)

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)

(SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) => SOrd (a, b, c, d, e, f, g)

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)

(%<) :: 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)

(%<=) :: 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)

(%>) :: 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)

(%>=) :: 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)

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)

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)

type family Comparing a a a where ...

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)

thenCmp returns its second argument if its first is EQ; otherwise, it returns its first argument.

thenCmp :: Ordering -> Ordering -> Ordering

type family ThenCmp a a where ...

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)

type family Sing

The singleton kind-indexed type family.

Instances

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SBool

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SOrdering

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SNat

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SSymbol

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple0

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SVoid

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAll

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAny

type Sing

Defined in Data.Singletons.TypeError

type Sing = SErrorMessage

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SList :: [a] -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SMaybe :: Maybe a -> Type

type Sing

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.

Defined in Data.Singletons.TypeRepTYPE

type Sing = TypeRep :: TYPE rep -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMin :: Min a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMax :: Max a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SOption :: Option a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SIdentity :: Identity a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SDual :: Dual a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SSum :: Sum a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SProduct :: Product a -> Type

type Sing

Defined in Data.Singletons.Prelude.Ord

type Sing = SDown :: Down a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SEither :: Either a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple2 :: (a, b) -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup

type Sing = SArg :: Arg a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Proxy

type Sing = SProxy :: Proxy t -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple3 :: (a, b, c) -> Type

type Sing

Defined in Data.Singletons.Prelude.Const

type Sing = SConst :: Const a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple4 :: (a, b, c, d) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple5 :: (a, b, c, d, e) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple6 :: (a, b, c, d, e, f) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SOrdering z where

Constructors

SLT :: SOrdering ('LT :: Ordering)

SEQ :: SOrdering ('EQ :: Ordering)

SGT :: SOrdering ('GT :: Ordering)

Instances

TestCoercion SOrdering

Defined in Data.Singletons.Prelude.Instances

Methods

testCoercion :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (Coercion a b)

TestEquality SOrdering

Defined in Data.Singletons.Prelude.Instances

Methods

testEquality :: forall (a :: k) (b :: k). SOrdering a -> SOrdering b -> Maybe (a :~: b)

Show (SOrdering z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SOrdering z -> ShowS

show :: SOrdering z -> String

showList :: [SOrdering z] -> ShowS

data SDown z where

Constructors

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

Instances

SDecide a => TestCoercion (SDown :: Down a -> Type)

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)

Defined in Data.Singletons.Prelude.Ord

Methods

testEquality :: forall (a0 :: k) (b :: k). SDown a0 -> SDown b -> Maybe (a0 :~: b)

type family GetDown a where ...

Equations

GetDown ('Down field) = field

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

Defunctionalization symbols

data ThenCmpSym0 a6989586621679394586

Instances

SingI ThenCmpSym0

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ThenCmpSym0

SuppressUnusedWarnings ThenCmpSym0

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ThenCmpSym0 (a6989586621679394586 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

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

data ThenCmpSym1 a6989586621679394586 a6989586621679394587

Instances

SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d)

SuppressUnusedWarnings (ThenCmpSym1 a6989586621679394586 :: TyFun Ordering Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ThenCmpSym1 a6989586621679394586 :: TyFun Ordering Ordering -> Type) (a6989586621679394587 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type Apply (ThenCmpSym1 a6989586621679394586 :: TyFun Ordering Ordering -> Type) (a6989586621679394587 :: Ordering) = ThenCmpSym2 a6989586621679394586 a6989586621679394587

type ThenCmpSym2 (a6989586621679394586 :: Ordering) (a6989586621679394587 :: Ordering) = ThenCmp a6989586621679394586 a6989586621679394587 :: Ordering

type LTSym0 = 'LT :: Ordering

type EQSym0 = 'EQ :: Ordering

type GTSym0 = 'GT :: Ordering

data CompareSym0 a6989586621679383640

Instances

SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing CompareSym0

SuppressUnusedWarnings (CompareSym0 :: TyFun a (a ~> Ordering) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679383640 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a (a ~> Ordering) -> Type) (a6989586621679383640 :: a) = CompareSym1 a6989586621679383640

data CompareSym1 a6989586621679383640 a6989586621679383641

Instances

(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (CompareSym1 d)

SuppressUnusedWarnings (CompareSym1 a6989586621679383640 :: TyFun a Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym1 a6989586621679383640 :: TyFun a Ordering -> Type) (a6989586621679383641 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 a6989586621679383640 :: TyFun a Ordering -> Type) (a6989586621679383641 :: a) = CompareSym2 a6989586621679383640 a6989586621679383641

type CompareSym2 (a6989586621679383640 :: a) (a6989586621679383641 :: a) = Compare a6989586621679383640 a6989586621679383641 :: Ordering

data (<@#@$) a6989586621679383645 infix 4

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$)

SuppressUnusedWarnings ((<@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383645 :: a)

Defined in Data.Singletons.Prelude.Ord

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

data a6989586621679383645 <@#@$$ a6989586621679383646 infix 4

Instances

(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<@#@$$) d)

SuppressUnusedWarnings ((<@#@$$) a6989586621679383645 :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$$) a6989586621679383645 :: TyFun a Bool -> Type) (a6989586621679383646 :: a)

Defined in Data.Singletons.Prelude.Ord

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

type (<@#@$$$) (a6989586621679383645 :: a) (a6989586621679383646 :: a) = (<) a6989586621679383645 a6989586621679383646 :: Bool infix 4

data (<=@#@$) a6989586621679383650 infix 4

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<=@#@$)

SuppressUnusedWarnings ((<=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Ord

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

data a6989586621679383650 <=@#@$$ a6989586621679383651 infix 4

Instances

(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((<=@#@$$) d)

SuppressUnusedWarnings ((<=@#@$$) a6989586621679383650 :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Ord

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

type (<=@#@$$$) (a6989586621679383650 :: a) (a6989586621679383651 :: a) = (<=) a6989586621679383650 a6989586621679383651 :: Bool infix 4

data (>@#@$) a6989586621679383655 infix 4

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$)

SuppressUnusedWarnings ((>@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383655 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383655 :: a) = (>@#@$$) a6989586621679383655

data a6989586621679383655 >@#@$$ a6989586621679383656 infix 4

Instances

(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>@#@$$) d)

SuppressUnusedWarnings ((>@#@$$) a6989586621679383655 :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$$) a6989586621679383655 :: TyFun a Bool -> Type) (a6989586621679383656 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) a6989586621679383655 :: TyFun a Bool -> Type) (a6989586621679383656 :: a) = a6989586621679383655 >@#@$$$ a6989586621679383656

type (>@#@$$$) (a6989586621679383655 :: a) (a6989586621679383656 :: a) = (>) a6989586621679383655 a6989586621679383656 :: Bool infix 4

data (>=@#@$) a6989586621679383660 infix 4

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>=@#@$)

SuppressUnusedWarnings ((>=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383660 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679383660 :: a) = (>=@#@$$) a6989586621679383660

data a6989586621679383660 >=@#@$$ a6989586621679383661 infix 4

Instances

(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ((>=@#@$$) d)

SuppressUnusedWarnings ((>=@#@$$) a6989586621679383660 :: TyFun a Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$$) a6989586621679383660 :: TyFun a Bool -> Type) (a6989586621679383661 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) a6989586621679383660 :: TyFun a Bool -> Type) (a6989586621679383661 :: a) = a6989586621679383660 >=@#@$$$ a6989586621679383661

type (>=@#@$$$) (a6989586621679383660 :: a) (a6989586621679383661 :: a) = (>=) a6989586621679383660 a6989586621679383661 :: Bool infix 4

data MaxSym0 a6989586621679383665

Instances

SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0

SuppressUnusedWarnings (MaxSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679383665 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679383665 :: a) = MaxSym1 a6989586621679383665

data MaxSym1 a6989586621679383665 a6989586621679383666

Instances

(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MaxSym1 d)

SuppressUnusedWarnings (MaxSym1 a6989586621679383665 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 a6989586621679383665 :: TyFun a a -> Type) (a6989586621679383666 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 a6989586621679383665 :: TyFun a a -> Type) (a6989586621679383666 :: a) = MaxSym2 a6989586621679383665 a6989586621679383666

type MaxSym2 (a6989586621679383665 :: a) (a6989586621679383666 :: a) = Max a6989586621679383665 a6989586621679383666 :: a

data MinSym0 a6989586621679383670

Instances

SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0

SuppressUnusedWarnings (MinSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679383670 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679383670 :: a) = MinSym1 a6989586621679383670

data MinSym1 a6989586621679383670 a6989586621679383671

Instances

(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (MinSym1 d)

SuppressUnusedWarnings (MinSym1 a6989586621679383670 :: TyFun a a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 a6989586621679383670 :: TyFun a a -> Type) (a6989586621679383671 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 a6989586621679383670 :: TyFun a a -> Type) (a6989586621679383671 :: a) = MinSym2 a6989586621679383670 a6989586621679383671

type MinSym2 (a6989586621679383670 :: a) (a6989586621679383671 :: a) = Min a6989586621679383670 a6989586621679383671 :: a

data ComparingSym0 a6989586621679383631

Instances

SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing ComparingSym0

SuppressUnusedWarnings (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) (a6989586621679383631 :: b ~> a)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type) (a6989586621679383631 :: b ~> a) = ComparingSym1 a6989586621679383631

data ComparingSym1 a6989586621679383631 a6989586621679383632

Instances

(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym1 d)

SuppressUnusedWarnings (ComparingSym1 a6989586621679383631 :: TyFun b (b ~> Ordering) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym1 a6989586621679383631 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679383632 :: b)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym1 a6989586621679383631 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679383632 :: b) = ComparingSym2 a6989586621679383631 a6989586621679383632

data ComparingSym2 a6989586621679383631 a6989586621679383632 a6989586621679383633

Instances

(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ComparingSym2 d1 d2)

SuppressUnusedWarnings (ComparingSym2 a6989586621679383631 a6989586621679383632 :: TyFun b Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym2 a6989586621679383631 a6989586621679383632 :: TyFun b Ordering -> Type) (a6989586621679383633 :: b)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym2 a6989586621679383631 a6989586621679383632 :: TyFun b Ordering -> Type) (a6989586621679383633 :: b) = ComparingSym3 a6989586621679383631 a6989586621679383632 a6989586621679383633

type ComparingSym3 (a6989586621679383631 :: (~>) b a) (a6989586621679383632 :: b) (a6989586621679383633 :: b) = Comparing a6989586621679383631 a6989586621679383632 a6989586621679383633 :: Ordering

data DownSym0 a6989586621679393010

Instances

SingI (DownSym0 :: TyFun a (Down a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0

SuppressUnusedWarnings (DownSym0 :: TyFun a (Down a) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (DownSym0 :: TyFun a (Down a) -> Type) (a6989586621679393010 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (DownSym0 :: TyFun a (Down a) -> Type) (a6989586621679393010 :: a) = DownSym1 a6989586621679393010

type DownSym1 (a6989586621679393010 :: a) = 'Down a6989586621679393010 :: Down (a :: Type)

data GetDownSym0 a6989586621679393013

Instances

SingI (GetDownSym0 :: TyFun (Down a) a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing GetDownSym0

SuppressUnusedWarnings (GetDownSym0 :: TyFun (Down a) a -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (GetDownSym0 :: TyFun (Down a) a -> Type) (a6989586621679393013 :: Down a)

Defined in Data.Singletons.Prelude.Ord

type Apply (GetDownSym0 :: TyFun (Down a) a -> Type) (a6989586621679393013 :: Down a) = GetDownSym1 a6989586621679393013

type GetDownSym1 (a6989586621679393013 :: Down (a :: Type)) = GetDown a6989586621679393013 :: a

Orphan instances

SingKind a => SingKind (Down a)

Associated Types

type Demote (Down a) = (r :: Type)

Methods

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

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

SDecide a => SDecide (Down a)

Methods

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

PEq (Down a)

Associated Types

type x == y :: Bool

type x /= y :: Bool

SEq a => SEq (Down a)

Methods

(%==) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Sing (a0 == b)

(%/=) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Sing (a0 /= b)

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

Methods

sing :: Sing ('Down0 n)