coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Jesse Clayton <j89clayton89 AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Stuck with functions.
- Date: Thu, 8 Nov 2012 06:29:21 -0500
There is an axiom in the FunctionalExtensionality module with signature [ functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g ]. Alternatively, you can use the [extensionality] tactic, which applies a variant of [functional_extensionality].
-Jason
On Thu, Nov 8, 2012 at 6:22 AM, Jesse Clayton <j89clayton89 AT gmail.com> wrote:
Hi,Variable K : Type.Lemma feq: forall (b : K -> K)(c : K -> K)(d : forall g, b g = c g), b = c.How can this be solved? Is there a predefined library for functions and similar stuff in Coq?Thanks.
- [Coq-Club] Stuck with functions., Jesse Clayton, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Jason Gross, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Adam Chlipala, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Dmitry Grebeniuk, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Kristopher Micinski, 11/08/2012
- Re: [Coq-Club] Stuck with functions., AUGER Cédric, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Jonas Oberhauser, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Daniel Schepler, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Jonas Oberhauser, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Daniel Schepler, 11/09/2012
- Re: [Coq-Club] Stuck with functions., AUGER Cédric, 11/09/2012
- Re: [Coq-Club] Stuck with functions., Jonas Oberhauser, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Alan Schmitt, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Daniel Schepler, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Jonas Oberhauser, 11/08/2012
- Re: [Coq-Club] Stuck with functions., Dmitry Grebeniuk, 11/08/2012
Archive powered by MHonArc 2.6.18.