type-level-0.2.4: Type-level programming library

Portabilitynon-portable
Stabilityexperimental (MPTC, non-standarad instances)
Maintaineralfonso.acosta@gmail.com

Data.TypeLevel.Bool

Contents

Description

Type-level Booleans.

Synopsis

Type-level boolean values

class BoolI b => Bool b Source

Type-level Booleans

Instances

BoolI b => Bool b 

toBool :: BoolI b => b -> BoolSource

data False Source

False type-level value

Instances

Show False 
Typeable False 
BoolI False 
Not False True 
Not True False 
IsZero D9 False 
IsZero D8 False 
IsZero D7 False 
IsZero D6 False 
IsZero D5 False 
IsZero D4 False 
IsZero D3 False 
IsZero D2 False 
IsZero D1 False 
Eq False False True 
Eq False True False 
Eq True False False 
Imp False False True 
Imp False True True 
Imp True False False 
Xor False False False 
Xor False True True 
Xor True False True 
Xor True True False 
Or False False False 
Or False True True 
Or True False True 
And False False False 
And False True False 
And True False False 
(Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd 
Nat x => GCD' x x False EQ x 
(Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd 
(Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT 
Succ xi yi => Succ' xi D9 yi D0 False 
Succ' xi D8 xi D9 False 
Succ' xi D7 xi D8 False 
Succ' xi D6 xi D7 False 
Succ' xi D5 xi D6 False 
Succ' xi D4 xi D5 False 
Succ' xi D3 xi D4 False 
Succ' xi D2 xi D3 False 
Succ' xi D1 xi D2 False 
Succ' xi D0 xi D1 False 
Pos x => IsZero (:* x d) False 

false :: FalseSource

False value-level reflecting function

data True Source

True type-level value

Instances

true :: TrueSource

True value-level reflecting function

reifyBool :: Bool -> (forall b. Bool b => b -> r) -> rSource

Reification function. In CPS style (best possible solution)

Type-level boolean operations

class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1Source

Boolean negation type-level relation. Not b1 b2 establishes that not b1 = b2

Instances

not :: Not b1 b2 => b1 -> b2Source

value-level reflection function for the Not type-level relation

class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3Source

And type-level relation. And b1 b2 b3 establishes that b1 && b2 = b3

(&&) :: And b1 b2 b3 => b1 -> b2 -> b3Source

value-level reflection function for the And type-level relation

class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3Source

Or type-level relation. Or b1 b2 b3 establishes that b1 || b2 = b3

(||) :: Or b1 b2 b3 => b1 -> b2 -> b3Source

value-level reflection function for the Or type-level relation

class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3Source

Exclusive or type-level relation. Xor b1 b2 b3 establishes that xor b1 b2 = b3

xor :: Xor b1 b2 b3 => b1 -> b2 -> b3Source

value-level reflection function for the Xor type-level relation

class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3Source

Implication type-level relation. Imp b1 b2 b3 establishes that b1 =>b2 = b3

imp :: Imp b1 b2 b3 => b1 -> b2 -> b3Source

value-level reflection function for the Imp type-level relation

class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3Source

Boolean equality type-level relation

eq :: Eq b1 b2 b3 => b1 -> b2 -> b3Source

value-level reflection function for the Eq type-level relation