|
Data.TypeLevel.Bool | Portability | non-portable | Stability | experimental (MPTC, non-standarad instances) | Maintainer | alfonso.acosta@gmail.com |
|
|
|
|
|
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 | |
|
|
toBool :: BoolI b => b -> Bool |
|
data False |
False type-level value
| Instances | |
|
|
false :: False |
False value-level reflecting function
|
|
data True |
True type-level value
| Instances | |
|
|
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 :: 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 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 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 :: 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 :: 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 :: Eq b1 b2 b3 => b1 -> b2 -> b3 |
value-level reflection function for the Eq type-level relation
|
|
Produced by Haddock version 2.6.0 |