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

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

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

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

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 [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 (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 (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 (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

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_6989586621679325222Sym0 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_6989586621679325255Sym0 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_6989586621679325288Sym0 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_6989586621679325321Sym0 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_6989586621679325354Sym0 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_6989586621679325387Sym0 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_6989586621679325420Sym0 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 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 [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 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 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 :: TyFun b a -> Type) (a :: b) (a :: b) :: Ordering where ...

Equations

Comparing p x y = Apply (Apply CompareSym0 (Apply p x)) (Apply p y)

sComparing :: forall (t :: TyFun b a -> Type) (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 (a :: k)

The singleton kind-indexed data family.

Instances

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

Defined in Data.Singletons.Decide

Methods

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

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

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.TypeRepStar

Methods

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

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

Ord (Sing a)

Defined in Data.Singletons.TypeRepStar

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.TypeRepStar

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, 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 (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (a :: Type)

Defined in Data.Singletons.TypeRepStar

data Sing (a :: Type) = STypeRep (TypeRep a)

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [k])
• SCons :: Sing (n ': n)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n :| n)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple2 :: Sing ((,) 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 (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

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

• STuple3 :: Sing ((,,) n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple4 :: Sing ((,,,) n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple5 :: Sing ((,,,,) n n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple6 :: Sing ((,,,,,) n n n n n n)

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

Defined in Data.Singletons.Prelude.Instances

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

• STuple7 :: Sing ((,,,,,,) n n n n n n n)

Defunctionalization symbols

data ThenCmpSym0 (l :: TyFun Ordering (TyFun Ordering Ordering -> Type))

Instances

SuppressUnusedWarnings ThenCmpSym0

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ThenCmpSym0 (l :: Ordering)

Defined in Data.Singletons.Prelude.Ord

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

data ThenCmpSym1 (l :: Ordering) (l :: TyFun Ordering Ordering)

Instances

SuppressUnusedWarnings ThenCmpSym1

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ThenCmpSym1 l1 :: TyFun Ordering Ordering -> *) (l2 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type Apply (ThenCmpSym1 l1 :: TyFun Ordering Ordering -> *) (l2 :: Ordering) = ThenCmp l1 l2

type ThenCmpSym2 (t :: Ordering) (t :: Ordering) = ThenCmp t t

type LTSym0 = LT

type EQSym0 = EQ

type GTSym0 = GT

data CompareSym0 (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Ordering -> Type))

Instances

SuppressUnusedWarnings (CompareSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Ordering -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Ordering -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Ordering -> Type) -> *) (l :: a6989586621679323527) = CompareSym1 l

data CompareSym1 (l :: a6989586621679323527) (l :: TyFun a6989586621679323527 Ordering)

Instances

SuppressUnusedWarnings (CompareSym1 :: a6989586621679323527 -> TyFun a6989586621679323527 Ordering -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (CompareSym1 l1 :: TyFun a Ordering -> *) (l2 :: a) = Compare l1 l2

type CompareSym2 (t :: a6989586621679323527) (t :: a6989586621679323527) = Compare t t

data (<@#@$) (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type))

Instances

SuppressUnusedWarnings ((<@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527) = (<@#@$$) l

data (l :: a6989586621679323527) <@#@$$ (l :: TyFun a6989586621679323527 Bool)

Instances

SuppressUnusedWarnings ((<@#@$$) :: a6989586621679323527 -> TyFun a6989586621679323527 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 < l2

type (<@#@$$$) (t :: a6989586621679323527) (t :: a6989586621679323527) = (<) t t

data (<=@#@$) (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type))

Instances

SuppressUnusedWarnings ((<=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527) = (<=@#@$$) l

data (l :: a6989586621679323527) <=@#@$$ (l :: TyFun a6989586621679323527 Bool)

Instances

SuppressUnusedWarnings ((<=@#@$$) :: a6989586621679323527 -> TyFun a6989586621679323527 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((<=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 <= l2

type (<=@#@$$$) (t :: a6989586621679323527) (t :: a6989586621679323527) = (<=) t t

data (>@#@$) (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type))

Instances

SuppressUnusedWarnings ((>@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527) = (>@#@$$) l

data (l :: a6989586621679323527) >@#@$$ (l :: TyFun a6989586621679323527 Bool)

Instances

SuppressUnusedWarnings ((>@#@$$) :: a6989586621679323527 -> TyFun a6989586621679323527 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 > l2

type (>@#@$$$) (t :: a6989586621679323527) (t :: a6989586621679323527) = (>) t t

data (>=@#@$) (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type))

Instances

SuppressUnusedWarnings ((>=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$) :: TyFun a6989586621679323527 (TyFun a6989586621679323527 Bool -> Type) -> *) (l :: a6989586621679323527) = (>=@#@$$) l

data (l :: a6989586621679323527) >=@#@$$ (l :: TyFun a6989586621679323527 Bool)

Instances

SuppressUnusedWarnings ((>=@#@$$) :: a6989586621679323527 -> TyFun a6989586621679323527 Bool -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply ((>=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 >= l2

type (>=@#@$$$) (t :: a6989586621679323527) (t :: a6989586621679323527) = (>=) t t

data MaxSym0 (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type))

Instances

SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *) (l :: a6989586621679323527) = MaxSym1 l

data MaxSym1 (l :: a6989586621679323527) (l :: TyFun a6989586621679323527 a6989586621679323527)

Instances

SuppressUnusedWarnings (MaxSym1 :: a6989586621679323527 -> TyFun a6989586621679323527 a6989586621679323527 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) = Max l1 l2

type MaxSym2 (t :: a6989586621679323527) (t :: a6989586621679323527) = Max t t

data MinSym0 (l :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type))

Instances

SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *) (l :: a6989586621679323527)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679323527 (TyFun a6989586621679323527 a6989586621679323527 -> Type) -> *) (l :: a6989586621679323527) = MinSym1 l

data MinSym1 (l :: a6989586621679323527) (l :: TyFun a6989586621679323527 a6989586621679323527)

Instances

SuppressUnusedWarnings (MinSym1 :: a6989586621679323527 -> TyFun a6989586621679323527 a6989586621679323527 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) = Min l1 l2

type MinSym2 (t :: a6989586621679323527) (t :: a6989586621679323527) = Min t t

data ComparingSym0 (l :: TyFun (TyFun b6989586621679323517 a6989586621679323516 -> Type) (TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> Type))

Instances

SuppressUnusedWarnings (ComparingSym0 :: TyFun (TyFun b6989586621679323517 a6989586621679323516 -> Type) (TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym0 :: TyFun (TyFun b6989586621679323517 a6989586621679323516 -> Type) (TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> Type) -> *) (l :: TyFun b6989586621679323517 a6989586621679323516 -> Type)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym0 :: TyFun (TyFun b6989586621679323517 a6989586621679323516 -> Type) (TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> Type) -> *) (l :: TyFun b6989586621679323517 a6989586621679323516 -> Type) = ComparingSym1 l

data ComparingSym1 (l :: TyFun b6989586621679323517 a6989586621679323516 -> Type) (l :: TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type))

Instances

SuppressUnusedWarnings (ComparingSym1 :: (TyFun b6989586621679323517 a6989586621679323516 -> Type) -> TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym1 l1 :: TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> *) (l2 :: b6989586621679323517)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym1 l1 :: TyFun b6989586621679323517 (TyFun b6989586621679323517 Ordering -> Type) -> *) (l2 :: b6989586621679323517) = ComparingSym2 l1 l2

data ComparingSym2 (l :: TyFun b6989586621679323517 a6989586621679323516 -> Type) (l :: b6989586621679323517) (l :: TyFun b6989586621679323517 Ordering)

Instances

SuppressUnusedWarnings (ComparingSym2 :: (TyFun b6989586621679323517 a6989586621679323516 -> Type) -> b6989586621679323517 -> TyFun b6989586621679323517 Ordering -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (ComparingSym2 l1 l2 :: TyFun b Ordering -> *) (l3 :: b)

Defined in Data.Singletons.Prelude.Ord

type Apply (ComparingSym2 l1 l2 :: TyFun b Ordering -> *) (l3 :: b) = Comparing l1 l2 l3

type ComparingSym3 (t :: TyFun b6989586621679323517 a6989586621679323516 -> Type) (t :: b6989586621679323517) (t :: b6989586621679323517) = Comparing t t t