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
- [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Jason Gross, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Jason Gross, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Interactive 'match' tactic (or treating 'case' more like 'match')?, Adam Chlipala, 07/14/2013
Archive powered by MHonArc 2.6.18.