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 |
Defines the class SDecide
, allowing for decidable equality over singletons.
The SDecide class
class kparam ~ KProxy => SDecide kparam whereSource
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.
(%~) :: forall a b. Sing a -> Sing b -> Decision (a :~: b)Source
Compute a proof or disproof of equality, given two singletons.
Supporting definitions
data a :~: b where
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
A logically uninhabited data type.