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 |
Data.Singletons.Decide
Description
Defines the class SDecide
, allowing for decidable equality over singletons.
The SDecide class
class SDecide k where Source #
Members of the SDecide
"kind" class support decidable equality. Instances
of this class are generated alongside singleton definitions for datatypes that
derive an Eq
instance.
Minimal complete definition
Supporting definitions
data (k :~: a) b :: forall k. 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
Uninhabited data type
Since: 4.8.0.0
A Decision
about a type a
is either a proof of existence or a proof that a
cannot exist.
Orphan instances
SDecide k2 => TestEquality k2 (Sing k2) Source # | |