Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Reference is not found

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reference is not found


Chronological Thread 
  • From: AUGER Cédric <sedrikov AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Reference is not found
  • Date: Wed, 23 Jan 2013 17:54:20 +0100

Le Wed, 23 Jan 2013 23:51:29 +0800,
liheng
<lihengszh AT gmail.com>
a écrit :

> Hello.
> The error occurs when runs *x * x + y * x + (x + y) * y = x * x + 2 *
> x
> * y + y * y *on*rewrite_mult_plus_distr_r?
> *I don't know the problem and the reasons.*
> *thanks*?
>
> **code is:*
> Require Import Arith.
> Lemma time2 : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.
> Proof.
> intros x y.
> SearchRewrite (_ * (_ + _)).
> rewrite mult_plus_distr_l.
> SearchRewrite ((_ + _) * _).
> rewrite mult_plus_distr_r with (p:=x).
> rewrite_mult_plus_distr_r.
> ...
> *Error: *
> The reference rewrite_mult_plus_distr_r was not found in the current
> environment.

Just remove your underscore…
rewrite mult_plus_distr_r

instead of

rewrite_mult_plus_distr_r



Archive powered by MHonArc 2.6.18.

Top of Page