coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] fun <-> forall

From: Burak Ekici <ekcburak AT hotmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] fun <-> forall
Date: Thu, 26 Oct 2017 11:09:12 +0000
Accept-language: tr-TR, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ekcburak AT hotmail.com; spf=Pass smtp.mailfrom=ekcburak AT hotmail.com; spf=Pass smtp.helo=postmaster AT EUR02-VE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:6XpykhCpuu7MQdcxgJtJUyQJP3N1i/DPJgcQr6AfoPdwSP3zr8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6lX71zMZGw3+OAxpPay1X9eK14Xkn9y1rrbUek1jgCe3Ked5KwzzpgHMvOEXh5FjI+A/0E2ajGFPfrF82HlhJhq+nBf354/k8Z1o+TlKsvEJ98lcVKz7e+IzSrkOX2duCHw8+MC+7UqLdgCI/HZJFzxOyhc=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi all,

I have an hypothesis of the following form "H : (fun a b f => XX a b f)
= (fun a b f => YY a b f)".

Is there a way to turn it into "H: forall a b f, XX a b f = YY a b f"?

Thanks!

Best,

―

Burak.

[Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
  - Re: [Coq-Club] fun <-> forall, Robbert Krebbers, 10/26/2017
    - Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
      - Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        Message not available
        Re: [Coq-Club] fun <-> forall, Samuel Gruetter, 10/28/2017
        [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
        Re: [Coq-Club] Macro for Ltac, Pierre Courtieu, 10/30/2017