tfp-1.0: Type-level integers, booleans, lists using type families

Safe HaskellSafe-Inferred
LanguageHaskell2010

Type.Data.Ord

Documentation

type family Compare x y Source

Instances

type Compare False False = EQ 
type Compare False True = LT 
type Compare True False = GT 
type Compare True True = EQ 
type Compare GT GT = EQ 
type Compare GT EQ = GT 
type Compare GT LT = GT 
type Compare EQ GT = LT 
type Compare EQ EQ = EQ 
type Compare EQ LT = GT 
type Compare LT GT = LT 
type Compare LT EQ = LT 
type Compare LT LT = EQ 
type Compare (Dec x) (Dec y) = Compare x y 

compare :: Proxy x -> Proxy y -> Proxy (Compare x y) Source

data LT Source

Instances

type IsGT LT = False 
type IsEQ LT = False 
type IsLT LT = True 
type Compare GT LT = GT 
type Compare EQ LT = GT 
type Compare LT GT = LT 
type Compare LT EQ = LT 
type Compare LT LT = EQ 

data EQ Source

Instances

type IsGT EQ = False 
type IsEQ EQ = True 
type IsLT EQ = False 
type Compare GT EQ = GT 
type Compare EQ GT = LT 
type Compare EQ EQ = EQ 
type Compare EQ LT = GT 
type Compare LT EQ = LT 

data GT Source

Instances

type IsGT GT = True 
type IsEQ GT = False 
type IsLT GT = False 
type Compare GT GT = EQ 
type Compare GT EQ = GT 
type Compare GT LT = GT 
type Compare EQ GT = LT 
type Compare LT GT = LT 

type family IsLT c Source

Instances

type IsLT GT = False 
type IsLT EQ = False 
type IsLT LT = True 

isLT :: Proxy c -> Proxy (IsLT c) Source

type family IsEQ c Source

Instances

type IsEQ GT = False 
type IsEQ EQ = True 
type IsEQ LT = False 

isEQ :: Proxy c -> Proxy (IsEQ c) Source

type family IsGT c Source

Instances

type IsGT GT = True 
type IsGT EQ = False 
type IsGT LT = False 

isGT :: Proxy c -> Proxy (IsGT c) Source

class x :<: y Source

lt :: Proxy x -> Proxy y -> Proxy (LTT x y) Source

type family LTT x y Source

Instances

type LTT x y = IsLT (Compare x y) 

class x :<=: y Source

le :: Proxy x -> Proxy y -> Proxy (LET x y) Source

type family LET x y Source

Instances

type LET x y = Not (GTT x y) 

class x :==: y Source

eq :: Proxy x -> Proxy y -> Proxy (EQT x y) Source

type family EQT x y Source

Instances

type EQT x y = IsEQ (Compare x y) 

class x :/=: y Source

ne :: Proxy x -> Proxy y -> Proxy (NET x y) Source

type family NET x y Source

Instances

type NET x y = Not (EQT x y) 

class x :>=: y Source

ge :: Proxy x -> Proxy y -> Proxy (GET x y) Source

type family GET x y Source

Instances

type GET x y = Not (LTT x y) 

class x :>: y Source

gt :: Proxy x -> Proxy y -> Proxy (GTT x y) Source

type family GTT x y Source

Instances

type GTT x y = IsGT (Compare x y) 

type family Min x y Source

Instances

type Min x y = If (LET x y) x y 

min :: Proxy x -> Proxy y -> Proxy (Min x y) Source

type family Max x y Source

Instances

type Max x y = If (GET x y) x y 

max :: Proxy x -> Proxy y -> Proxy (Max x y) Source