Data.Ord.Singletons

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_6989586621679178639Sym0 a) a

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

type a < a = Apply (Apply TFHelper_6989586621679178660Sym0 a) a

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

type a <= a = Apply (Apply TFHelper_6989586621679178676Sym0 a) a

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

type a > a = Apply (Apply TFHelper_6989586621679178692Sym0 a) a

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

type a >= a = Apply (Apply TFHelper_6989586621679178708Sym0 a) a

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

type Max a a = Apply (Apply Max_6989586621679178724Sym0 a) a

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

type Min a a = Apply (Apply Min_6989586621679178740Sym0 a) a

Instances

POrd All

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Any

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Void

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Ordering

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Natural

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd ()

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Bool

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Char

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd Symbol

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Identity a)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (First a)

Defined in Data.Monoid.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Last a)

Defined in Data.Monoid.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Down a)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (First a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Last a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Max a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Min a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Product a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (NonEmpty a)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Maybe a)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd [a]

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Either a b)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Proxy s)

Defined in Data.Proxy.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Arg a b)

Defined in Data.Semigroup.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (Const a b)

Defined in Data.Functor.Const.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

POrd (a, b, c, d)

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

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

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

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

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

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

Defined in Data.Ord.Singletons

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: 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_6989586621679178639Sym0 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_6989586621679178660Sym0 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_6989586621679178676Sym0 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_6989586621679178692Sym0 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_6989586621679178708Sym0 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_6989586621679178724Sym0 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_6989586621679178740Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t :: a)

Instances

SOrd Bool => SOrd All

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

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

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

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

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

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

SOrd Bool => SOrd Any

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

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

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

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

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

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

SOrd Void

Defined in Data.Ord.Singletons

Methods

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

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

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

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

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

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

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

SOrd Ordering

Defined in Data.Ord.Singletons

Methods

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

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

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

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

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

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

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

SOrd Natural

Defined in GHC.TypeLits.Singletons.Internal

Methods

sCompare :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd ()

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

sMax :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd Bool

Defined in Data.Ord.Singletons

Methods

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

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

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

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

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

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

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

SOrd Char

Defined in GHC.TypeLits.Singletons.Internal

Methods

sCompare :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SOrd Symbol

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Identity a)

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Monoid.Singletons

Methods

sCompare :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Monoid.Singletons

Methods

sCompare :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Down a)

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (First a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Last a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Max a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Max a) (t2 :: Max a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Min a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Min a) (t2 :: Min a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd m => SOrd (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: WrappedMonoid m) (t2 :: WrappedMonoid m). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Dual a) (t2 :: Dual a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Product a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Product a) (t2 :: Product a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Methods

sCompare :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Maybe a)

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

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

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd (Proxy s)

Defined in Data.Proxy.Singletons

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Arg a b)

Defined in Data.Semigroup.Singletons

Methods

sCompare :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

SOrd a => SOrd (Const a b)

Defined in Data.Functor.Const.Singletons

Methods

sCompare :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Defined in Data.Ord.Singletons

Methods

sCompare :: forall (t1 :: (a, b, c, d, e, f)) (t2 :: (a, b, c, d, e, f)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

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

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

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

Methods

sCompare :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

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

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

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

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

sMax :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

type family Comparing (a :: (~>) b a) (a :: b) (a :: b) :: Ordering 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 :: Ordering) (a :: Ordering) :: Ordering 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 :: k -> Type

Instances

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SAll

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SAny

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SVoid

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SOrdering

type Sing

Defined in Data.Singletons.Base.TypeError

type Sing = SErrorMessage

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SNat

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = STuple0

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SBool

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SChar

type Sing

Defined in GHC.TypeLits.Singletons.Internal

type Sing = SSymbol

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SIdentity :: Identity a -> Type

type Sing

Defined in Data.Monoid.Singletons

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Monoid.Singletons

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Ord.Singletons

type Sing = SDown :: Down a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SMax :: Max a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SMin :: Min a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SDual :: Dual a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SProduct :: Product a -> Type

type Sing

Defined in Data.Semigroup.Singletons.Internal

type Sing = SSum :: Sum a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type

type Sing

Defined in Data.Singletons.Base.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.Base.TypeRepTYPE

type Sing = TypeRep :: TYPE rep -> Type

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Proxy.Singletons

type Sing = SProxy :: Proxy t -> Type

type Sing

Defined in Data.Semigroup.Singletons

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

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons

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

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Functor.Const.Singletons

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

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Functor.Product.Singletons

type Sing = SProduct :: Product f g a -> Type

type Sing

Defined in Data.Functor.Sum.Singletons

type Sing = SSum :: Sum f g a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Functor.Compose.Singletons

type Sing = SCompose :: Compose f g a -> Type

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Singletons.Base.Instances

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

type Sing

Defined in Data.Singletons.Base.Instances

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

data SOrdering :: Ordering -> Type where

Constructors

SLT :: SOrdering ('LT :: Ordering)

SEQ :: SOrdering ('EQ :: Ordering)

SGT :: SOrdering ('GT :: Ordering)

Instances

TestCoercion SOrdering

Defined in Data.Singletons.Base.Instances

Methods

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

TestEquality SOrdering

Defined in Data.Singletons.Base.Instances

Methods

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

Show (SOrdering z)

Defined in Data.Singletons.Base.Instances

Methods

showsPrec :: Int -> SOrdering z -> ShowS

show :: SOrdering z -> String

showList :: [SOrdering z] -> ShowS

data SDown :: forall (a :: Type). Down a -> Type 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.Ord.Singletons

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

Methods

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

type family GetDown (a :: Down (a :: Type)) :: 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 :: (~>) Ordering ((~>) Ordering Ordering)

Instances

SingI ThenCmpSym0

Defined in Data.Ord.Singletons

Methods

sing :: Sing ThenCmpSym0

SuppressUnusedWarnings ThenCmpSym0

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ThenCmpSym0 (a6989586621679178589 :: Ordering)

Defined in Data.Ord.Singletons

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

data ThenCmpSym1 (a6989586621679178589 :: Ordering) :: (~>) Ordering Ordering

Instances

SingI1 ThenCmpSym1

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (ThenCmpSym1 x)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ThenCmpSym1 d)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (ThenCmpSym1 a6989586621679178589 :: TyFun Ordering Ordering -> Type) (a6989586621679178590 :: Ordering)

Defined in Data.Ord.Singletons

type Apply (ThenCmpSym1 a6989586621679178589 :: TyFun Ordering Ordering -> Type) (a6989586621679178590 :: Ordering) = ThenCmp a6989586621679178589 a6989586621679178590

type family ThenCmpSym2 (a6989586621679178589 :: Ordering) (a6989586621679178590 :: Ordering) :: Ordering where ...

Equations

ThenCmpSym2 a6989586621679178589 a6989586621679178590 = ThenCmp a6989586621679178589 a6989586621679178590

type family LTSym0 :: Ordering where ...

Equations

LTSym0 = 'LT

type family EQSym0 :: Ordering where ...

Equations

EQSym0 = 'EQ

type family GTSym0 :: Ordering where ...

Equations

GTSym0 = 'GT

data CompareSym0 :: (~>) a ((~>) a Ordering)

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing CompareSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data CompareSym1 (a6989586621679178605 :: a) :: (~>) a Ordering

Instances

SOrd a => SingI1 (CompareSym1 :: a -> TyFun a Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (CompareSym1 x)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (CompareSym1 d)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym1 a6989586621679178605 :: TyFun a Ordering -> Type) (a6989586621679178606 :: a)

Defined in Data.Ord.Singletons

type Apply (CompareSym1 a6989586621679178605 :: TyFun a Ordering -> Type) (a6989586621679178606 :: a) = Compare a6989586621679178605 a6989586621679178606

type family CompareSym2 (a6989586621679178605 :: a) (a6989586621679178606 :: a) :: Ordering where ...

Equations

CompareSym2 a6989586621679178605 a6989586621679178606 = Compare a6989586621679178605 a6989586621679178606

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

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (<@#@$)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data (<@#@$$) (a6989586621679178610 :: a) :: (~>) a Bool infix 4

Instances

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

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ((<@#@$$) x)

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$$) a6989586621679178610 :: TyFun a Bool -> Type) (a6989586621679178611 :: a)

Defined in Data.Ord.Singletons

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

type family (a6989586621679178610 :: a) <@#@$$$ (a6989586621679178611 :: a) :: Bool where ... infix 4

Equations

a6989586621679178610 <@#@$$$ a6989586621679178611 = (<) a6989586621679178610 a6989586621679178611

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

Instances

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data (<=@#@$$) (a6989586621679178615 :: a) :: (~>) a Bool infix 4

Instances

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

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ((<=@#@$$) x)

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

type family (a6989586621679178615 :: a) <=@#@$$$ (a6989586621679178616 :: a) :: Bool where ... infix 4

Equations

a6989586621679178615 <=@#@$$$ a6989586621679178616 = (<=) a6989586621679178615 a6989586621679178616

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

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (>@#@$)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data (>@#@$$) (a6989586621679178620 :: a) :: (~>) a Bool infix 4

Instances

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

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ((>@#@$$) x)

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$$) a6989586621679178620 :: TyFun a Bool -> Type) (a6989586621679178621 :: a)

Defined in Data.Ord.Singletons

type Apply ((>@#@$$) a6989586621679178620 :: TyFun a Bool -> Type) (a6989586621679178621 :: a) = a6989586621679178620 > a6989586621679178621

type family (a6989586621679178620 :: a) >@#@$$$ (a6989586621679178621 :: a) :: Bool where ... infix 4

Equations

a6989586621679178620 >@#@$$$ a6989586621679178621 = (>) a6989586621679178620 a6989586621679178621

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

Instances

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data (>=@#@$$) (a6989586621679178625 :: a) :: (~>) a Bool infix 4

Instances

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

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ((>=@#@$$) x)

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

Defined in Data.Ord.Singletons

Methods

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

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$$) a6989586621679178625 :: TyFun a Bool -> Type) (a6989586621679178626 :: a)

Defined in Data.Ord.Singletons

type Apply ((>=@#@$$) a6989586621679178625 :: TyFun a Bool -> Type) (a6989586621679178626 :: a) = a6989586621679178625 >= a6989586621679178626

type family (a6989586621679178625 :: a) >=@#@$$$ (a6989586621679178626 :: a) :: Bool where ... infix 4

Equations

a6989586621679178625 >=@#@$$$ a6989586621679178626 = (>=) a6989586621679178625 a6989586621679178626

data MaxSym0 :: (~>) a ((~>) a a)

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing MaxSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data MaxSym1 (a6989586621679178630 :: a) :: (~>) a a

Instances

SOrd a => SingI1 (MaxSym1 :: a -> TyFun a a -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (MaxSym1 x)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MaxSym1 d)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 a6989586621679178630 :: TyFun a a -> Type) (a6989586621679178631 :: a)

Defined in Data.Ord.Singletons

type Apply (MaxSym1 a6989586621679178630 :: TyFun a a -> Type) (a6989586621679178631 :: a) = Max a6989586621679178630 a6989586621679178631

type family MaxSym2 (a6989586621679178630 :: a) (a6989586621679178631 :: a) :: a where ...

Equations

MaxSym2 a6989586621679178630 a6989586621679178631 = Max a6989586621679178630 a6989586621679178631

data MinSym0 :: (~>) a ((~>) a a)

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing MinSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data MinSym1 (a6989586621679178635 :: a) :: (~>) a a

Instances

SOrd a => SingI1 (MinSym1 :: a -> TyFun a a -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (MinSym1 x)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MinSym1 d)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 a6989586621679178635 :: TyFun a a -> Type) (a6989586621679178636 :: a)

Defined in Data.Ord.Singletons

type Apply (MinSym1 a6989586621679178635 :: TyFun a a -> Type) (a6989586621679178636 :: a) = Min a6989586621679178635 a6989586621679178636

type family MinSym2 (a6989586621679178635 :: a) (a6989586621679178636 :: a) :: a where ...

Equations

MinSym2 a6989586621679178635 a6989586621679178636 = Min a6989586621679178635 a6989586621679178636

data ComparingSym0 :: (~>) ((~>) b a) ((~>) b ((~>) b Ordering))

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing ComparingSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

data ComparingSym1 (a6989586621679178596 :: (~>) b a) :: (~>) b ((~>) b Ordering)

Instances

SOrd a => SingI1 (ComparingSym1 :: (b ~> a) -> TyFun b (b ~> Ordering) -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (ComparingSym1 x)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym1 d)

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym1 a6989586621679178596 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679178597 :: b)

Defined in Data.Ord.Singletons

type Apply (ComparingSym1 a6989586621679178596 :: TyFun b (b ~> Ordering) -> Type) (a6989586621679178597 :: b) = ComparingSym2 a6989586621679178596 a6989586621679178597

data ComparingSym2 (a6989586621679178596 :: (~>) b a) (a6989586621679178597 :: b) :: (~>) b Ordering

Instances

(SOrd a, SingI d) => SingI1 (ComparingSym2 d :: b -> TyFun b Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing :: forall (x :: k1). Sing x -> Sing (ComparingSym2 d x)

SOrd a => SingI2 (ComparingSym2 :: (b ~> a) -> b -> TyFun b Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (ComparingSym2 x y)

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym2 d1 d2)

SuppressUnusedWarnings (ComparingSym2 a6989586621679178596 a6989586621679178597 :: TyFun b Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym2 a6989586621679178596 a6989586621679178597 :: TyFun b Ordering -> Type) (a6989586621679178598 :: b)

Defined in Data.Ord.Singletons

type Apply (ComparingSym2 a6989586621679178596 a6989586621679178597 :: TyFun b Ordering -> Type) (a6989586621679178598 :: b) = Comparing a6989586621679178596 a6989586621679178597 a6989586621679178598

type family ComparingSym3 (a6989586621679178596 :: (~>) b a) (a6989586621679178597 :: b) (a6989586621679178598 :: b) :: Ordering where ...

Equations

ComparingSym3 a6989586621679178596 a6989586621679178597 a6989586621679178598 = Comparing a6989586621679178596 a6989586621679178597 a6989586621679178598

data DownSym0 :: (~>) a (Down (a :: Type))

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing DownSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

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

type family DownSym1 (a6989586621679190229 :: a) :: Down (a :: Type) where ...

Equations

DownSym1 a6989586621679190229 = 'Down a6989586621679190229

data GetDownSym0 :: (~>) (Down (a :: Type)) a

Instances

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

Defined in Data.Ord.Singletons

Methods

sing :: Sing GetDownSym0

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

Defined in Data.Ord.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Ord.Singletons

type Apply (GetDownSym0 :: TyFun (Down a) a -> Type) (a6989586621679190232 :: Down a) = GetDown a6989586621679190232

type family GetDownSym1 (a6989586621679190232 :: Down (a :: Type)) :: a where ...

Equations

GetDownSym1 a6989586621679190232 = GetDown a6989586621679190232

Orphan instances

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

Methods

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

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 arg == arg1 :: Bool

type arg /= arg1 :: Bool

SEq a => SEq (Down a)

Methods

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

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

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

Methods

sing :: Sing ('Down n)