coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about examples of TypeClass in reference-manual

From: Zhaohui Li <lizhaohui1991 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about examples of TypeClass in reference-manual
Date: Sun, 12 Jun 2016 09:07:28 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lizhaohui1991 AT gmail.com; spf=Pass smtp.mailfrom=lizhaohui1991 AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f174.google.com
Ironport-phdr: 9a23:Q2oGeRKMSj0XgdJ3h9mcpTZWNBhigK39O0sv0rFitYgUKfXxwZ3uMQTl6Ol3ixeRBMOAu6MC1Lud6fi4EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35XxiLH5ocWLKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs0kcW2IWjxsAJwmNuBX7TJf4tSvnt7MsiXCyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW

Thanks very much for all help!

"Generalizable All Variables" works for me.

2016-06-11 21:35 GMT+08:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Robert,

ah yes, thanks for the reminder!

@Zhaohui: this backquote magic is described in chapter "2.7.19 Implicit generalization" of the reference manual.

Best regards,

Michael

-----Original Message-----
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Robbert Krebbers
Sent: Saturday, June 11, 2016 3:25 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about examples of TypeClass in reference-manual

You need to set

Generalizable All Variables.

for that.

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Question about examples of TypeClass in reference-manual, Zhaohui Li, 06/11/2016
- Re: [Coq-Club] Question about examples of TypeClass in reference-manual, Jean-Marie Madiot, 06/11/2016
  - RE: [Coq-Club] Question about examples of TypeClass in reference-manual, Soegtrop, Michael, 06/11/2016
    - Re: [Coq-Club] Question about examples of TypeClass in reference-manual, Robbert Krebbers, 06/11/2016
      - RE: [Coq-Club] Question about examples of TypeClass in reference-manual, Soegtrop, Michael, 06/11/2016
        
        Re: [Coq-Club] Question about examples of TypeClass in reference-manual, Zhaohui Li, 06/12/2016