coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] match/ proof of branch

From: Adam Chlipala <adam AT chlipala.net>
To: Marco Servetto <marco.servetto AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] match/ proof of branch
Date: Wed, 13 Jul 2011 08:35:33 -0400

gallais @ ensl.org wrote:

Have you tried something using a [return] in your [match]?

Sorry for misinterpreting the question! FYI, CPDT, which I referenced, includes this trick and many related ones, so my boneheaded answer wasn't a total wash. ;)

[Coq-Club] match/ proof of branch, marco . servetto
- Re: [Coq-Club] match/ proof of branch, Adam Chlipala
  - Re: [Coq-Club] match/ proof of branch, Marco Servetto
    - Re: [Coq-Club] match/ proof of branch, gallais @ ensl.org
      - Re: [Coq-Club] match/ proof of branch, Adam Chlipala
      - Re: [Coq-Club] match/ proof of branch, Marco Servetto
        
        Re: [Coq-Club] match/ proof of branch, Pierre Courtieu
        
        Re: [Coq-Club] match/ proof of branch, AUGER Cedric
- Re: [Coq-Club] match/ proof of branch, Marco Servetto
  - Re: [Coq-Club] match/ proof of branch, Adam Chlipala
    - Re: [Coq-Club] match/ proof of branch, Adam Chlipala
    - Re: [Coq-Club] match/ proof of branch, gallais @ ensl.org
      - Re: [Coq-Club] match/ proof of branch, Adam Chlipala
        
        Re: [Coq-Club] match/ proof of branch, Marco Servetto
        
        Re: [Coq-Club] match/ proof of branch, Adam Chlipala