coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Chlipala <adamc AT csail.mit.edu>
To: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Matching parameters of dependent types with common stem
Date: Wed, 03 Oct 2012 13:29:24 -0400

Have you read CPDT <http://adam.chlipala.net/cpdt/>? There is extensive discussion there of issues like yours.

[Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Pierre Boutillier, 10/03/2012
  - Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/03/2012
    - Re: [Coq-Club] Matching parameters of dependent types with common stem, Adam Chlipala, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Robbert Krebbers, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, AUGER Cédric, 10/03/2012
  - Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/04/2012
    - Re: [Coq-Club] Matching parameters of dependent types with common stem, AUGER Cédric, 10/04/2012