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

License | BSD-style (see LICENSE) |

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

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

Defines the class `SDecide`

, allowing for decidable equality over singletons.

# The SDecide class

# Supporting definitions

data a :~: b :: k -> k -> * where infix 4

Propositional equality. If `a :~: b`

is inhabited by some terminating
value, then the type `a`

is the same as the type `b`

. To use this equality
in practice, pattern-match on the `a :~: b`

to get out the `Refl`

constructor;
in the body of the pattern-match, the compiler knows that `a ~ b`

.

*Since: 4.7.0.0*

data Void :: *

Uninhabited data type

*Since: 4.8.0.0*