Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] replace ... at?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] replace ... at?


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page