coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
- To: Jonas Oberhauser <s9joober AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] replace ... at?
- Date: Thu, 4 Oct 2012 10:46:51 -0400
On 4 oct. 2012, at 09:54, Jonas Oberhauser
<s9joober AT gmail.com>
wrote:
> Hi all,
>
> is there such a thing like a replace at?
>
> Goal forall X (x y : X) P, P x y -> x = y -> P x x.
> intros.
> replace x with y at 2. (* doesn't work ? *)
> rewrite H at 2. (* supposedly requries Setoid ? *)
Hi,
indeed the at requires Setoid, and there is a variant
[setoid_replace] defined in theories/Classes/SetoidTactics.v.
It will rewrite with standard leibniz equality just as well
as rewrite.
Best,
-- Matthieu
- [Coq-Club] replace ... at?, Jonas Oberhauser, 10/04/2012
- Re: [Coq-Club] replace ... at?, Lucian M. Patcas, 10/04/2012
- Re: [Coq-Club] replace ... at?, Jonas Oberhauser, 10/05/2012
- Re: [Coq-Club] replace ... at?, Matthieu Sozeau, 10/04/2012
- Re: [Coq-Club] replace ... at?, Jonas Oberhauser, 10/05/2012
- Re: [Coq-Club] replace ... at?, Lucian M. Patcas, 10/04/2012
Archive powered by MHonArc 2.6.18.