Data.Singletons.Prelude.Ord

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

Documentation

class PEq a => POrd (a :: Type)

Associated Types

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

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

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

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

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

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

type Min (arg :: a) (arg :: 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 (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)

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

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

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

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

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

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

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

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

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

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

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

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

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

Instances

SOrd Bool

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd Ordering

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

SOrd Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

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

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

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

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

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

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

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

SOrd ()

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd Void

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd Bool => SOrd All

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd Bool => SOrd Any

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Maybe a)

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd m => SOrd (WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

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

SOrd a => SOrd (Identity a)

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

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

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

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

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

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

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

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

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

Defined in Data.Singletons.Prelude.Monoid

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

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

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

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

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

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

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

SOrd a => SOrd (Down a)

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

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

SOrd a => SOrd (Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

Methods

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

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

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

SOrd a => SOrd (Const a b)

Defined in Data.Singletons.Prelude.Const

Methods

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

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

sMin :: 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 :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

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

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

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

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

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

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

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

data family Sing :: k -> Type

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)

SDecide k => TestEquality (Sing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

testEquality :: Sing a -> Sing b -> Maybe (a :~: b)

Show (SSymbol s)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SSymbol s -> ShowS

show :: SSymbol s -> String

showList :: [SSymbol s] -> ShowS

Show (SNat n)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

Eq (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Ord (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

compare :: Sing a -> Sing a -> Ordering

(<) :: Sing a -> Sing a -> Bool

(<=) :: Sing a -> Sing a -> Bool

(>) :: Sing a -> Sing a -> Bool

(>=) :: Sing a -> Sing a -> Bool

max :: Sing a -> Sing a -> Sing a

min :: Sing a -> Sing a -> Sing a

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing [a]) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing a)

Defined in Data.Singletons.TypeRepTYPE

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing b) => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing m => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (Maybe a) => Show (Sing z)

Defined in Data.Singletons.Prelude.Monoid

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bool => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bool => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing a => Show (Sing z)

Defined in Data.Singletons.Prelude.Semigroup

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

(ShowSing a, ShowSing [a]) => Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (a :: PErrorMessage)

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

• SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
• SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
• (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
• (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

data Sing (b :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

• SNil :: forall k (b :: [k]). Sing ([] :: [k])
• SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)

data Sing (b :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (a :: TYPE rep)

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 -> Type` 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

data Sing (a :: TYPE rep) = STypeRep (TypeRep a)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

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

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :| n)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)

data Sing (c :: Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

• SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (d :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

• STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)

data Sing (c :: Const a b)

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

• SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)

data Sing (e :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

• STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)

data Sing (f :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

• STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)

data Sing (g :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

• STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)

data Sing (h :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

• STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

type SOrdering = (Sing :: Ordering -> Type)

type SDown = (Sing :: Down a -> Type)

Defunctionalization symbols

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

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 (a6989586621679391212 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

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

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (ThenCmpSym1 d)

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ThenCmpSym1 a6989586621679391212 :: TyFun Ordering Ordering -> Type) (a6989586621679391213 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type Apply (ThenCmpSym1 a6989586621679391212 :: TyFun Ordering Ordering -> Type) (a6989586621679391213 :: Ordering) = ThenCmp a6989586621679391212 a6989586621679391213

type ThenCmpSym2 (a6989586621679391212 :: Ordering) (a6989586621679391213 :: Ordering) = ThenCmp a6989586621679391212 a6989586621679391213

type LTSym0 = LT

type EQSym0 = EQ

type GTSym0 = GT

data CompareSym0 :: forall a6989586621679380707. (~>) a6989586621679380707 ((~>) a6989586621679380707 Ordering)

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing CompareSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> Ordering) -> Type) (arg6989586621679380801 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> Ordering) -> Type) (arg6989586621679380801 :: a6989586621679380707) = CompareSym1 arg6989586621679380801

data CompareSym1 (arg6989586621679380801 :: a6989586621679380707) :: (~>) a6989586621679380707 Ordering

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 arg6989586621679380801 :: TyFun a6989586621679380707 Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym1 arg6989586621679380801 :: TyFun a Ordering -> Type) (arg6989586621679380802 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 arg6989586621679380801 :: TyFun a Ordering -> Type) (arg6989586621679380802 :: a) = Compare arg6989586621679380801 arg6989586621679380802

type CompareSym2 (arg6989586621679380801 :: a6989586621679380707) (arg6989586621679380802 :: a6989586621679380707) = Compare arg6989586621679380801 arg6989586621679380802

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (<@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$) :: TyFun a6989586621679380707 (a6989586621679380707 ~> Bool) -> Type) (arg6989586621679380805 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

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

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

SuppressUnusedWarnings ((<@#@$$) arg6989586621679380805 :: TyFun a6989586621679380707 Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$$) arg6989586621679380805 :: TyFun a Bool -> Type) (arg6989586621679380806 :: a)

Defined in Data.Singletons.Prelude.Ord

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

type (<@#@$$$) (arg6989586621679380805 :: a6989586621679380707) (arg6989586621679380806 :: a6989586621679380707) = (<) arg6989586621679380805 arg6989586621679380806

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Ord

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

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

SuppressUnusedWarnings ((<=@#@$$) arg6989586621679380809 :: TyFun a6989586621679380707 Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Ord

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

type (<=@#@$$$) (arg6989586621679380809 :: a6989586621679380707) (arg6989586621679380810 :: a6989586621679380707) = (<=) arg6989586621679380809 arg6989586621679380810

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing (>@#@$)

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$) :: TyFun a6989586621679380707 (a6989586621679380707 ~> Bool) -> Type) (arg6989586621679380813 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a6989586621679380707 (a6989586621679380707 ~> Bool) -> Type) (arg6989586621679380813 :: a6989586621679380707) = (>@#@$$) arg6989586621679380813

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

SuppressUnusedWarnings ((>@#@$$) arg6989586621679380813 :: TyFun a6989586621679380707 Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$$) arg6989586621679380813 :: TyFun a Bool -> Type) (arg6989586621679380814 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) arg6989586621679380813 :: TyFun a Bool -> Type) (arg6989586621679380814 :: a) = arg6989586621679380813 > arg6989586621679380814

type (>@#@$$$) (arg6989586621679380813 :: a6989586621679380707) (arg6989586621679380814 :: a6989586621679380707) = (>) arg6989586621679380813 arg6989586621679380814

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$) :: TyFun a6989586621679380707 (a6989586621679380707 ~> Bool) -> Type) (arg6989586621679380817 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a6989586621679380707 (a6989586621679380707 ~> Bool) -> Type) (arg6989586621679380817 :: a6989586621679380707) = (>=@#@$$) arg6989586621679380817

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

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

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

SuppressUnusedWarnings ((>=@#@$$) arg6989586621679380817 :: TyFun a6989586621679380707 Bool -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$$) arg6989586621679380817 :: TyFun a Bool -> Type) (arg6989586621679380818 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) arg6989586621679380817 :: TyFun a Bool -> Type) (arg6989586621679380818 :: a) = arg6989586621679380817 >= arg6989586621679380818

type (>=@#@$$$) (arg6989586621679380817 :: a6989586621679380707) (arg6989586621679380818 :: a6989586621679380707) = (>=) arg6989586621679380817 arg6989586621679380818

data MaxSym0 :: forall a6989586621679380707. (~>) a6989586621679380707 ((~>) a6989586621679380707 a6989586621679380707)

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MaxSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> a6989586621679380707) -> Type) (arg6989586621679380821 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> a6989586621679380707) -> Type) (arg6989586621679380821 :: a6989586621679380707) = MaxSym1 arg6989586621679380821

data MaxSym1 (arg6989586621679380821 :: a6989586621679380707) :: (~>) a6989586621679380707 a6989586621679380707

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 arg6989586621679380821 :: TyFun a6989586621679380707 a6989586621679380707 -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 arg6989586621679380821 :: TyFun a a -> Type) (arg6989586621679380822 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 arg6989586621679380821 :: TyFun a a -> Type) (arg6989586621679380822 :: a) = Max arg6989586621679380821 arg6989586621679380822

type MaxSym2 (arg6989586621679380821 :: a6989586621679380707) (arg6989586621679380822 :: a6989586621679380707) = Max arg6989586621679380821 arg6989586621679380822

data MinSym0 :: forall a6989586621679380707. (~>) a6989586621679380707 ((~>) a6989586621679380707 a6989586621679380707)

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing MinSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> a6989586621679380707) -> Type) (arg6989586621679380825 :: a6989586621679380707)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679380707 (a6989586621679380707 ~> a6989586621679380707) -> Type) (arg6989586621679380825 :: a6989586621679380707) = MinSym1 arg6989586621679380825

data MinSym1 (arg6989586621679380825 :: a6989586621679380707) :: (~>) a6989586621679380707 a6989586621679380707

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 arg6989586621679380825 :: TyFun a6989586621679380707 a6989586621679380707 -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 arg6989586621679380825 :: TyFun a a -> Type) (arg6989586621679380826 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 arg6989586621679380825 :: TyFun a a -> Type) (arg6989586621679380826 :: a) = Min arg6989586621679380825 arg6989586621679380826

type MinSym2 (arg6989586621679380825 :: a6989586621679380707) (arg6989586621679380826 :: a6989586621679380707) = Min arg6989586621679380825 arg6989586621679380826

data ComparingSym0 :: forall a6989586621679380696 b6989586621679380697. (~>) ((~>) b6989586621679380697 a6989586621679380696) ((~>) b6989586621679380697 ((~>) b6989586621679380697 Ordering))

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 (b6989586621679380697 ~> a6989586621679380696) (b6989586621679380697 ~> (b6989586621679380697 ~> Ordering)) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym0 :: TyFun (b6989586621679380697 ~> a6989586621679380696) (b6989586621679380697 ~> (b6989586621679380697 ~> Ordering)) -> Type) (a6989586621679380792 :: b6989586621679380697 ~> a6989586621679380696)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym0 :: TyFun (b6989586621679380697 ~> a6989586621679380696) (b6989586621679380697 ~> (b6989586621679380697 ~> Ordering)) -> Type) (a6989586621679380792 :: b6989586621679380697 ~> a6989586621679380696) = ComparingSym1 a6989586621679380792

data ComparingSym1 (a6989586621679380792 :: (~>) b6989586621679380697 a6989586621679380696) :: (~>) b6989586621679380697 ((~>) b6989586621679380697 Ordering)

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 a6989586621679380792 :: TyFun b6989586621679380697 (b6989586621679380697 ~> Ordering) -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym1 a6989586621679380792 :: TyFun b6989586621679380697 (b6989586621679380697 ~> Ordering) -> Type) (a6989586621679380793 :: b6989586621679380697)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym1 a6989586621679380792 :: TyFun b6989586621679380697 (b6989586621679380697 ~> Ordering) -> Type) (a6989586621679380793 :: b6989586621679380697) = ComparingSym2 a6989586621679380792 a6989586621679380793

data ComparingSym2 (a6989586621679380792 :: (~>) b6989586621679380697 a6989586621679380696) (a6989586621679380793 :: b6989586621679380697) :: (~>) b6989586621679380697 Ordering

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 a6989586621679380793 a6989586621679380792 :: TyFun b6989586621679380697 Ordering -> Type)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym2 a6989586621679380793 a6989586621679380792 :: TyFun b Ordering -> Type) (a6989586621679380794 :: b)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym2 a6989586621679380793 a6989586621679380792 :: TyFun b Ordering -> Type) (a6989586621679380794 :: b) = Comparing a6989586621679380793 a6989586621679380792 a6989586621679380794

type ComparingSym3 (a6989586621679380792 :: (~>) b6989586621679380697 a6989586621679380696) (a6989586621679380793 :: b6989586621679380697) (a6989586621679380794 :: b6989586621679380697) = Comparing a6989586621679380792 a6989586621679380793 a6989586621679380794

data DownSym0 :: forall (a6989586621679092637 :: Type). (~>) a6989586621679092637 (Down (a6989586621679092637 :: Type))

Instances

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

Defined in Data.Singletons.Prelude.Ord

Methods

sing :: Sing DownSym0

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

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Singletons.Prelude.Ord

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

type DownSym1 (t6989586621679389894 :: a6989586621679092637) = Down t6989586621679389894

Orphan instances

SingKind a => SingKind (Down a)

Associated Types

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

Methods

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

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

SDecide a => SDecide (Down a)

Methods

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

(%==) :: Sing a0 -> Sing b -> Sing (a0 == b)

(%/=) :: Sing a0 -> Sing b -> Sing (a0 /= b)

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

Methods

sing :: Sing (Down0 n)

SingI (TyCon1 (Down :: a -> Down a) :: a ~> Down a)

Methods

sing :: Sing (TyCon1 Down0)