Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?


Chronological Thread 
  • From: Michiel Helvensteijn <mhelvens AT gmail.com>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?
  • Date: Sun, 14 Jul 2013 17:14:12 +0200

On Sun, Jul 14, 2013 at 4:37 PM, Adam Chlipala
<adamc AT csail.mit.edu>
wrote:

> Have you read CPDT <http://adam.chlipala.net/cpdt/>?

I've "seen" it. :-) I'll be happy to have a closer look.

> I suggest looking into an even more automated proof style (described in
> CPDT),

Sounds good. Could you perhaps point me to the right chapter or give
me an example of the technique you would recommend in my case?

It will be a long while before I have time to give it a comprehensive read.

> where there is no inherent case order in your scripts, not even at the level
> found in your first script below.

The only inherent case order in my `match` script is that the wildcard
pattern never matches `case2` because it is given last. And that might
actually be considered a "good thing", as it saves typing.

--
www.mhelvens.net



Archive powered by MHonArc 2.6.18.

Top of Page