What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?
$\begingroup$
$\endgroup$
-
2$\begingroup$ Some motivation and background for the question would be helpful. Please see the tips about how to write a better question section of our FAQ. $\endgroup$ – Kaveh Apr 14 '13 at 17:48
$\begingroup$
$\endgroup$
Your question is very brief, so my answer will be as well:
Structure DecidableEquivalenceRelation :=
{
carrier :> Type ;
rel :> carrier -> carrier -> Prop ;
reflexive : forall x, rel x x ;
symmetric : forall x y, rel x y -> rel y x ;
transitive : forall x y z, rel x y -> rel y z -> rel x y ;
decidable : forall x y, (rel x y) + ~ (rel x y)
}.
answered Apr 15 '13 at 6:20
