coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Michael <michaelschausten AT googlemail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Match goal with
- Date: Sun, 15 Aug 2010 12:48:18 -0400
Michael wrote:
Besides, I'm not very skilled with the syntax of Ltac, especially "match goal
with". Is there maybe a good tutorial with examples you can recommend?
This is one of the main focuses of the book I'm working on:
http://adam.chlipala.net/cpdt/
- [Coq-Club] Match goal with, Michael
- Re: [Coq-Club] Match goal with, Stéphane Glondu
- Re: [Coq-Club] Match goal with, Adam Chlipala
Archive powered by MhonArc 2.6.16.