singletons-1.1.1: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

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 Source

type arg :>= arg :: Bool Source

type arg :> arg :: Bool Source

type arg :<= arg :: Bool Source

type Max arg arg :: a Source

type Min arg arg :: a Source

Instances

POrd Bool (KProxy Bool) 
POrd Ordering (KProxy Ordering) 
POrd Nat (KProxy Nat) 
POrd Symbol (KProxy Symbol) 
POrd () (KProxy ()) 
POrd [k] (KProxy [k]) 
POrd (Maybe k) (KProxy (Maybe k)) 
POrd (Either k k) (KProxy (Either k k)) 
POrd ((,) k k) (KProxy ((,) k k)) 
POrd ((,,) k k k) (KProxy ((,,) k k k)) 
POrd ((,,,) k k k k) (KProxy ((,,,) k k k k)) 
POrd ((,,,,) k k k k k) (KProxy ((,,,,) k k k k k)) 
POrd ((,,,,,) k k k k k k) (KProxy ((,,,,,) k k k k k k)) 
POrd ((,,,,,,) k k k k k k k) (KProxy ((,,,,,,) k k k k k k k)) 

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

Minimal complete definition

Nothing

Methods

sCompare :: forall x y. Sing x -> Sing y -> Sing (Compare x y) Source

(%:<) :: forall x y. Sing x -> Sing y -> Sing (x :< y) Source

(%:<=) :: forall x y. Sing x -> Sing y -> Sing (x :<= y) Source

(%:>) :: forall x y. Sing x -> Sing y -> Sing (x :> y) Source

(%:>=) :: forall x y. Sing x -> Sing y -> Sing (x :>= y) Source

sMax :: forall x y. Sing x -> Sing y -> Sing (Max x y) Source

sMin :: forall x y. Sing x -> Sing y -> Sing (Min x y) 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 = LTSym0 
ThenCmp GT z = GTSym0 

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

data family Sing a Source

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *) 
SDecide k (KProxy k) => TestEquality k (Sing k) 
data Sing Bool where 
data Sing Ordering where 
data Sing * where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

Defunctionalization symbols

type ThenCmpSym2 t t = ThenCmp t t Source

data CompareSym0 l Source

Instances

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

data CompareSym1 l l Source

Instances

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

type CompareSym2 t t = Compare t t Source

data (:<$) l Source

Instances

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

data l :<$$ l Source

Instances

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

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

data (:<=$) l Source

Instances

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

data l :<=$$ l Source

Instances

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

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

data (:>$) l Source

Instances

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

data l :>$$ l Source

Instances

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

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

data (:>=$) l Source

Instances

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

data l :>=$$ l Source

Instances

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

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

data MaxSym0 l Source

Instances

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

data MaxSym1 l l Source

Instances

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

type MaxSym2 t t = Max t t Source

data MinSym0 l Source

Instances

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

data MinSym1 l l Source

Instances

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

type MinSym2 t t = Min t t Source