Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Ord

Contents

Defunctionalization symbols

Description

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

Synopsis

Documentation

class (PEq (KProxy :: KProxy a), kproxy ~ KProxy) => POrd kproxy Source

Associated Types

type Compare arg arg :: Ordering Source

type arg :< arg :: Bool infix 4 Source

type arg :<= arg :: Bool infix 4 Source

type arg :> arg :: Bool infix 4 Source

type arg :>= arg :: Bool infix 4 Source

type Max arg arg :: a Source

type Min arg arg :: a Source

Instances

POrd Bool (KProxy Bool) Source
POrd Ordering (KProxy Ordering) Source
POrd () (KProxy ()) Source
POrd [a] (KProxy [a]) Source
POrd (Maybe a) (KProxy (Maybe a)) Source
POrd (Either a b) (KProxy (Either a b)) Source
POrd ((,) a b) (KProxy ((,) a b)) Source
POrd ((,,) a b c) (KProxy ((,,) a b c)) Source
POrd ((,,,) a b c d) (KProxy ((,,,) a b c d)) Source
POrd ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) Source
POrd ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) Source
POrd ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) Source

class (SEq (KProxy :: KProxy a), kproxy ~ KProxy) => SOrd kproxy where Source

Minimal complete definition

Nothing

Methods

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

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

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

(%:>) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:>$) t) t :: Bool) infix 4 Source

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

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

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

Instances

SOrd Bool (KProxy Bool) Source
SOrd Ordering (KProxy Ordering) Source
SOrd () (KProxy ()) Source
(SOrd a0 (KProxy a0), SOrd [a0] (KProxy [a0])) => SOrd [a] (KProxy [a]) Source
SOrd a0 (KProxy a0) => SOrd (Maybe a) (KProxy (Maybe a)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0)) => SOrd (Either a b) (KProxy (Either a b)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0)) => SOrd ((,) a b) (KProxy ((,) a b)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0)) => SOrd ((,,) a b c) (KProxy ((,,) a b c)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0)) => SOrd ((,,,) a b c d) (KProxy ((,,,) a b c d)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0)) => SOrd ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0), SOrd f0 (KProxy f0)) => SOrd ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) Source
(SOrd a0 (KProxy a0), SOrd b0 (KProxy b0), SOrd c0 (KProxy c0), SOrd d0 (KProxy d0), SOrd e0 (KProxy e0), SOrd f0 (KProxy f0), SOrd g0 (KProxy g0)) => SOrd ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) Source

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

thenCmp :: Ordering -> Ordering -> Ordering Source

type family ThenCmp a a :: Ordering Source

Equations

ThenCmp EQ x = x
ThenCmp LT _z_1627574913 = LTSym0
ThenCmp GT _z_1627574916 = GTSym0

sThenCmp :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ThenCmpSym0 t) t :: Ordering) Source

data family Sing a Source

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z False => Sing Bool z STrue :: (~) Bool z True => Sing Bool z Source
data Sing Ordering where SLT :: (~) Ordering z LT => Sing Ordering z SEQ :: (~) Ordering z EQ => Sing Ordering z SGT :: (~) Ordering z GT => Sing Ordering z Source
data Sing * where STypeRep :: Typeable * a => Sing * a Source
data Sing Nat where SNat :: KnownNat n => Sing Nat n Source
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n Source
data Sing () where STuple0 :: (~) () z () => Sing () z Source
data Sing [a0] where SNil :: (~) [a] z ([] a) => Sing [a] z SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z Source
data Sing (Maybe a0) where SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z Source
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) } Source
data Sing (Either a0 b0) where SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z Source
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z Source
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z Source
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z Source
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z Source
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z Source
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z Source

Defunctionalization symbols

data ThenCmpSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Ordering (TyFun Ordering Ordering -> ) -> ) ThenCmpSym0 Source
type Apply (TyFun Ordering Ordering -> *) Ordering ThenCmpSym0 l0 = ThenCmpSym1 l0 Source

data ThenCmpSym1 l l Source

Instances

SuppressUnusedWarnings (Ordering -> TyFun Ordering Ordering -> *) ThenCmpSym1 Source
type Apply Ordering Ordering (ThenCmpSym1 l1) l0 = ThenCmpSym2 l1 l0 Source

type ThenCmpSym2 t t = ThenCmp t t Source

type LTSym0 = LT Source

type EQSym0 = EQ Source

type GTSym0 = GT Source

data CompareSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Ordering -> ) -> ) (CompareSym0 k) Source
type Apply (TyFun k Ordering -> *) k (CompareSym0 k) l0 = CompareSym1 k l0 Source

data CompareSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Ordering -> *) (CompareSym1 k) Source
type Apply Ordering k (CompareSym1 k l1) l0 = CompareSym2 k l1 l0 Source

type CompareSym2 t t = Compare t t Source

data (:<$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> ) -> ) ((:<$) k) Source
type Apply (TyFun k Bool -> *) k ((:<$) k) l0 = (:<$$) k l0 Source

data l :<$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:<$$) k) Source
type Apply Bool k ((:<$$) k l1) l0 = (:<$$$) k l1 l0 Source

type (:<$$$) t t = (:<) t t Source

data (:<=$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> ) -> ) ((:<=$) k) Source
type Apply (TyFun k Bool -> *) k ((:<=$) k) l0 = (:<=$$) k l0 Source

data l :<=$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:<=$$) k) Source
type Apply Bool k ((:<=$$) k l1) l0 = (:<=$$$) k l1 l0 Source

type (:<=$$$) t t = (:<=) t t Source

data (:>$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> ) -> ) ((:>$) k) Source
type Apply (TyFun k Bool -> *) k ((:>$) k) l0 = (:>$$) k l0 Source

data l :>$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:>$$) k) Source
type Apply Bool k ((:>$$) k l1) l0 = (:>$$$) k l1 l0 Source

type (:>$$$) t t = (:>) t t Source

data (:>=$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> ) -> ) ((:>=$) k) Source
type Apply (TyFun k Bool -> *) k ((:>=$) k) l0 = (:>=$$) k l0 Source

data l :>=$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:>=$$) k) Source
type Apply Bool k ((:>=$$) k l1) l0 = (:>=$$$) k l1 l0 Source

type (:>=$$$) t t = (:>=) t t Source

data MaxSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> ) -> ) (MaxSym0 k) Source
type Apply (TyFun k k -> *) k (MaxSym0 k) l0 = MaxSym1 k l0 Source

data MaxSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) (MaxSym1 k) Source
type Apply k k (MaxSym1 k l1) l0 = MaxSym2 k l1 l0 Source

type MaxSym2 t t = Max t t Source

data MinSym0 l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> ) -> ) (MinSym0 k) Source
type Apply (TyFun k k -> *) k (MinSym0 k) l0 = MinSym1 k l0 Source

data MinSym1 l l Source

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) (MinSym1 k) Source
type Apply k k (MinSym1 k l1) l0 = MinSym2 k l1 l0 Source

type MinSym2 t t = Min t t Source