coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] More dependent pattern matching

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: Adam Chlipala <adamc AT hcoop.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] More dependent pattern matching
Date: Mon, 9 Jun 2008 15:21:09 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Adam,

That's a great idea. In fact, we already use a similar solution
elsewhere in the development; it just didn't occur to me to use it here
too. Thanks for the suggestion!

Edsko

[Coq-Club] More dependent pattern matching, Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching, Adam Chlipala
  - Re: [Coq-Club] More dependent pattern matching, Edsko de Vries
  - Re: [Coq-Club] More dependent pattern matching, Conor McBride
    - Re: [Coq-Club] More dependent pattern matching, Conor McBride
    - Re: [Coq-Club] More dependent pattern matching, Edsko de Vries
      - Re: [Coq-Club] More dependent pattern matching, Conor McBride
- <Possible follow-ups>
- Re: [Coq-Club] More dependent pattern matching, rcp