Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Stuck with functions.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Stuck with functions.


Chronological Thread 
  • 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.




Archive powered by MHonArc 2.6.18.

Top of Page