coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting and eta rule

From: Taral <taralx AT gmail.com>
To: Andrej Bauer <andrej.bauer AT andrej.com>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Rewriting and eta rule
Date: Mon, 1 Jun 2009 14:10:34 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=IHMYTE4K9svvkREDPK0GOb6ZN/qVwLKzCoN3lFUGvMZ7uNSmKaRb96g0nHb0jGf7T/ VNJ4lrHNYt+P3E/+e+h2FbKMPQS4/aJPf4jcXPYKo1CHlkqLL5P8Cvcfa42EaDjbEOa8 JkC6pQVQoWA6CeP6GncG04fafeQkat30/FAVw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Jun 1, 2009 at 10:58 AM, Andrej Bauer
<andrej.bauer AT andrej.com>
wrote:
> Lemma test1 (A B C : Set) (g : (A -> B) -> C) (f : A -> B): g (fun x
> => f x) = g f.
> Proof.
> �intros.

Implicit Arguments eta_rule [A B].
rewrite (eta_rule f).

If you want smarter, try this:

repeat match goal with |- context [fun z : _ => ?f z] => rewrite
(eta_rule f) end.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] Rewriting and eta rule, Andrej Bauer
- Re: Re[Coq-Club] writing and eta rule, muad
  - Re: Re[Coq-Club] writing and eta rule, Andrej Bauer
- Re: [Coq-Club] Rewriting and eta rule, Taral