Copyright | (C) 2013 Richard Eisenberg |
---|---|

License | (C) 2013 Richard Eisenberg |

Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

- The
`Bool`

singleton - Conditionals
- Singletons from
`Data.Bool`

Defines functions and datatypes relating to the singleton for `Bool`

,
including a singletons version of all the definitions in `Data.Bool`

.

Because many of these definitions are produced by Template Haskell,
it is not possible to create proper Haddock documentation. Please look
up the corresponding operation in `Data.Bool`

. Also, please excuse
the apparent repeated variable names. This is due to an interaction
between Template Haskell and Haddock.

- data family Sing a
- type SBool z = Sing z
- type family If cond tru fls :: k
- sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
- type family Not a :: Bool
- sNot :: SBool a -> SBool (Not a)
- type :&& a b = a && b
- type :|| a b = a || b
- (%:&&) :: SBool a -> SBool b -> SBool (a :&& b)
- (%:||) :: SBool a -> SBool b -> SBool (a :|| b)
- type family Bool_ a a a :: a
- sBool_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Bool_ t t t)
- type Otherwise = True
- sOtherwise :: Sing Otherwise

# The `Bool`

singleton

Though Haddock doesn't show it, the `Sing`

instance above declares
constructors

SFalse :: Sing False STrue :: Sing True

# Conditionals

# Singletons from `Data.Bool`

The following are derived from the function `bool`

in `Data.Bool`

. The extra
underscore is to avoid name clashes with the type `Bool`

.