coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Question about examples of TypeClass in reference-manual
Date: Sat, 11 Jun 2016 13:35:25 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga03.intel.com
Ironport-phdr: 9a23:p/PoLxY9En6ahxK9EKXUmIb/LSx+4OfEezUN459isYplN5qZpcu7bnLW6fgltlLVR4KTs6sC0LqH9f+xEjFRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0pMyYPlQArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Ku4zSqUdBzA7OUg04tfqvF/NV0HHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jWOhOsD5UaozQXDqyqZgSBbljG1PYzs4+2Heh8g2l6VWrw67oARXwojIbYXTP/17KPCONegGTHZMC54CHxdKBZmxOtMC

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