coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Rui Baptista <rpgcbaptista AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Rewriting with equivalence relations in Set / Type
- Date: Thu, 27 Feb 2014 21:21:06 +0000
It works if I use
Hint Extern 1 => apply A1 : CompatHints.
Hint Extern 1 => apply A2 : CompatHints.
Hint Extern 1 => apply A3 : CompatHints.
Hint Extern 1 => apply A4 : CompatHints.
Hint Extern 1 => apply A5 : CompatHints.
Hint Extern 1 => apply A6 : CompatHints.
Hint Extern 1 => apply A7 : CompatHints.
Hint Extern 1 => apply A8 : CompatHints.
Hint Extern 1 => apply A9 : CompatHints.
Hint Extern 1 => apply A10 : CompatHints.
Hint Extern 1 => apply A11 : CompatHints.
instead of
Hint Resolve A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 : CompatHints.
But it's kind of slow, and I'm forced to use
Global Opaque not.
so it doesn't unfold not. Also, it prefers to use compatibility with universal quantification instead of implication.
I used refine (iff_backwards _ _ _ _) when I should have used refine (iff_forwards _ _ _ _).
- [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- <Possible follow-up(s)>
- [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Jason Gross, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Jason Gross, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Pierre-Marie Pédrot, 02/28/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/28/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Pierre-Marie Pédrot, 02/28/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Robbert Krebbers, 02/28/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Jason Gross, 02/27/2014
Archive powered by MHonArc 2.6.18.