coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types

From: Adam Chlipala <adamc AT hcoop.net>
To: Roman Beslik <beroal AT ukr.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types
Date: Tue, 03 Feb 2009 08:44:19 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Roman Beslik wrote:

Though I use
refine (f_equal (fun a => a b0) _).
instead of
generalize b0.
Are they the same?

You can find out for yourself by using both in proof scripts and running [Show Proof] (while still in interactive proof mode) or [Print <name-of-theorem>] (after finishing the proof with [Qed]).

[Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types, Roman Beslik
- Re: [Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types, Adam Chlipala
  - Re: [Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types, Roman Beslik
    - Re: [Coq-Club] dependent tuple, pattern-matching, extensional equality of functions, equal types, Adam Chlipala