|Copyright||(C) 2013 Richard Eisenberg|
|License||BSD-style (see LICENSE)|
|Maintainer||Richard Eisenberg (firstname.lastname@example.org)|
Defines the class
SDecide, allowing for decidable equality over singletons.
The SDecide class
Compute a proof or disproof of equality, given two singletons.
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
in the body of the pattern-match, the compiler knows that
a ~ b.
A logically uninhabited data type.