Data.Typelevel.Bool

data True

The type level True value.

Instances

• Show True
• BoolI True
• Not False True
• Not True False
• And False True False
• And True False False
• And True True True
• Or False True True
• Or True False True
• Or True True True
• Xor False True True
• Xor True False True
• Xor True True False
• Imp False False True
• Imp False True True
• Imp True False False
• Imp True True True
• Eq False False True
• Eq False True False
• Eq True False False
• Eq True True True

trueT :: True

data False

The type level False value.

Instances

• Show False
• BoolI False
• Not False True
• Not True False
• And False False False
• And False True False
• And True False False
• Or False False False
• Or False True True
• Or True False True
• Xor False False False
• Xor False True True
• Xor True False True
• Xor True True False
• Imp False False True
• Imp False True True
• Imp True False False
• Eq False False True
• Eq False True False
• Eq True False False

falseT :: False

class (BoolI b) <= Bool b 

A type level boolean constraint.

Use (Bool b) => b to express that the type b must be either True or False.

Instances

• (BoolI b) => Bool b

class BoolI b  where

Members

• toBool :: b -> Boolean

Instances

• BoolI True
• BoolI False

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

Convert a value level boolean into a type level boolean through a callback function.

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

Type level logical not.

(Not a b) => a -> b applies the constraint that a and b must be logical opposites.

Instances

• Not False True
• Not True False

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

Type level logical and.

(And a b c) => a -> b -> c applies the constraint that c must be the result of applying a logical and operation to a and b.

Instances

• And False False False
• And False True False
• And True False False
• And True True True

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

Type level logical or.

(Or a b c) => a -> b -> c applies the constraint that c must be the result of applying a logical or operation to a and b.

Instances

• Or False False False
• Or False True True
• Or True False True
• Or True True True

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

Type level logical xor.

(Xor a b c) => a -> b -> c applies the constraint that c must be the result of applying a logical xor operation to a and b.

Instances

• Xor False False False
• Xor False True True
• Xor True False True
• Xor True True False

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

Type level logical implication.

(Imp a b c) => a -> b -> c applies the constraint that c must be the result of applying a logical implication operation to a and b.

Instances

• Imp False False True
• Imp False True True
• Imp True False False
• Imp True True True

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

Boolean equality check.

(Eq a b c) => a -> b -> c applies the constraint that c must be the result of testing whether a and b are equal.

Instances

• Eq False False True
• Eq False True False
• Eq True False False
• Eq True True True

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

and :: forall b1 b2 b3. And b1 b2 b3 => b1 -> b2 -> b3

or :: forall b1 b2 b3. Or b1 b2 b3 => b1 -> b2 -> b3

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

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

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