singletons-2.0.1: A framework for generating singleton types

Data.Singletons.Prelude.Ord

Contents

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

 Source Source 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

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

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 whereSFalse :: (~) Bool z False => Sing Bool zSTrue :: (~) Bool z True => Sing Bool z Source data Sing Ordering whereSLT :: (~) Ordering z LT => Sing Ordering zSEQ :: (~) Ordering z EQ => Sing Ordering zSGT :: (~) Ordering z GT => Sing Ordering z Source data Sing * whereSTypeRep :: Typeable * a => Sing * a Source data Sing Nat whereSNat :: KnownNat n => Sing Nat n Source data Sing Symbol whereSSym :: KnownSymbol n => Sing Symbol n Source data Sing () whereSTuple0 :: (~) () z () => Sing () z Source data Sing [a0] whereSNil :: (~) [a] z ([] a) => Sing [a] zSCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z Source data Sing (Maybe a0) whereSNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) zSJust :: (~) (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) whereSLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) zSRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z Source data Sing ((,) a0 b0) whereSTuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z Source data Sing ((,,) a0 b0 c0) whereSTuple3 :: (~) ((,,) 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) whereSTuple4 :: (~) ((,,,) 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) whereSTuple5 :: (~) ((,,,,) 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) whereSTuple6 :: (~) ((,,,,,) 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) whereSTuple7 :: (~) ((,,,,,,) 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

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

data ThenCmpSym1 l l Source

Instances

 Source type Apply Ordering Ordering (ThenCmpSym1 l1) l0 = ThenCmpSym2 l1 l0 Source

type ThenCmpSym2 t t = ThenCmp t t 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