coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewriting with an equivalence relation that maps to Type

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Rewriting with an equivalence relation that maps to Type
Date: Fri, 4 Mar 2011 00:37:00 +0100

Is there a way to register an equivalence relation e : A -> A > Type
with "Add (Parametric) Relation"? Notice that it maps to Type, not
Prop. I seem to remember reading something about this, but I cannot
find it. I would like to use the rewriting mechanisms for such a
relation. Changing it to Prop is not an option.

With kind regards,

Andrej

[Coq-Club] Rewriting with an equivalence relation that maps to Type, Andrej Bauer
- Re: [Coq-Club] Rewriting with an equivalence relation that maps to Type, AUGER Cedric