type-level-0.2.4: Type-level programming library Contents Index

Data.TypeLevel.Bool Portability non-portable Stability experimental (MPTC, non-standarad instances) Maintainer alfonso.acosta@gmail.com

Contents Type-level boolean values Type-level boolean operations

Description

Type-level Booleans.

Synopsis

class BoolI b => Bool b toBool :: BoolI b => b -> Bool data False false :: False data True true :: True reifyBool :: Bool -> (forall b. Bool b => b -> r) -> r class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1 not :: Not b1 b2 => b1 -> b2 class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3 (&&) :: And b1 b2 b3 => b1 -> b2 -> b3 class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3 (||) :: Or b1 b2 b3 => b1 -> b2 -> b3 class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3 xor :: Xor b1 b2 b3 => b1 -> b2 -> b3 class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3 imp :: Imp b1 b2 b3 => b1 -> b2 -> b3 class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3 eq :: Eq b1 b2 b3 => b1 -> b2 -> b3

Type-level boolean values

class BoolI b => Bool b

Type-level Booleans Instances BoolI b => Bool b

toBool :: BoolI b => b -> Bool

data False

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 :: False

False value-level reflecting function

data True

True type-level value Instances Show True Typeable True BoolI True Not False True Not True False IsZero D0 True Eq False False True Eq False True False Eq True False False Eq True True True Imp False False True Imp False True True Imp True False False Imp True True True Xor False True True Xor True False True Xor True True False Or False True True Or True False True Or True True True And False True False And True False False And True True True Nat x => GCD' x D0 True cmp D0 (Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ Failure (PredecessorOfZeroError x) => Succ' (x, x) (x, x) D0 D0 True

true :: True

True value-level reflecting function

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

Reification function. In CPS style (best possible solution)

Type-level boolean operations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Boolean equality type-level relation Instances Eq False False True Eq False True False Eq True False False Eq True True True

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

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

Produced by Haddock version 2.6.0