coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Simplification for typeclass instances

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Simplification for typeclass instances
Date: Mon, 12 Sep 2016 16:03:17 +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 mga02.intel.com
Ironport-phdr: 9a23:M1UKIRe0EgUB50hUmqxBZQgclGMj4u6mDksu8pMizoh2WeGdxc6ybR7h7PlgxGXEQZ/co6odzbGH6ua+CSdRvN7B6ClEK80UEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUrDbg8n/7e2u4ZqbO1wO32vkJ+0iZ0Tr5UWJ749N0NMkcv5wgjLy4VJwM9xMwm1pIV/B1z3d3eyXuKBZziJLpvg6/NRBW6ipN44xTLhfESh0ezttvJ6j5lH/Sl7F7XwFF24SjxBgAg7f7Ri8UI27+n/xsfM40y2HN+X3S6o1UHKs9fE4ZgXvjXJNDDk0/33NjdQ0xIdaqxKoqhg1i9rRYYqVPfd6OLjacNwGX21ZdsdXSyFFRIi7at1cXKI6Ie9Eotyl9BM1phykCFz0CQ==

Dear Jonathan,

Indeed quite tricky. It would be nice to have some test cases.

Best regards,

Michael
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] Simplification for typeclass instances, Daniel Schepler, 09/09/2016
- Re: [Coq-Club] Simplification for typeclass instances, Jonathan Leivent, 09/09/2016
  - Re: [Coq-Club] Simplification for typeclass instances, Jonathan Leivent, 09/09/2016
    - RE: [Coq-Club] Simplification for typeclass instances, Soegtrop, Michael, 09/12/2016
      - RE: [Coq-Club] Simplification for typeclass instances, Soegtrop, Michael, 09/12/2016
        
        Re: [Coq-Club] Simplification for typeclass instances, Jonathan Leivent, 09/12/2016
        
        Re: [Coq-Club] Simplification for typeclass instances, Jason Gross, 09/12/2016
        
        RE: [Coq-Club] Simplification for typeclass instances, Soegtrop, Michael, 09/12/2016
        
        RE: [Coq-Club] Simplification for typeclass instances, Soegtrop, Michael, 09/12/2016
- Re: [Coq-Club] Simplification for typeclass instances, Gaetan Gilbert, 09/09/2016
  - Re: [Coq-Club] Simplification for typeclass instances, Daniel Schepler, 09/09/2016
    - Re: [Coq-Club] Simplification for typeclass instances, Gaetan Gilbert, 09/09/2016