coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rewrite A at 1 fails

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] rewrite A at 1 fails
Date: Thu, 13 Dec 2012 09:00:08 +0100

Why does the following application of "rewrite at" fail?

Require Import Setoid.

Lemma test X (f : X -> X -> Prop) x :
f x = (fun y => ~f y y) -> f x x = ~f x x.

Proof. intros A. rewrite A at 1.

(I know that I can use pattern)

Gert

[Coq-Club] rewrite A at 1 fails, Gert Smolka, 12/13/2012
- Re: [Coq-Club] rewrite A at 1 fails, Thomas Braibant, 12/13/2012
  - Re: [Coq-Club] rewrite A at 1 fails, AUGER Cédric, 12/13/2012
  - Re: [Coq-Club] rewrite A at 1 fails, Matthieu Sozeau, 12/13/2012
  - Re: [Coq-Club] rewrite A at 1 fails, Enrico Tassi, 12/13/2012
- Re: [Coq-Club] rewrite A at 1 fails, Beta Ziliani, 12/13/2012