Mercurial > cpdt > repo
comparison src/Intro.v @ 318:70e51e8cfce7
New InductiveTypes exercises and difficulty markings
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 12 Sep 2011 16:42:51 -0400 |
| parents | d5787b70cf48 |
| children | 06d11a6363cd |
comparison
equal
deleted
inserted
replaced
| 317:50db9a6e2742 | 318:70e51e8cfce7 |
|---|---|
| 166 Some readers have suggested that I give multiple recommended reading orders in this introduction, targeted at people with different levels of Coq expertise. It is certainly true that Part I of the book devotes significant space to basic concepts that most Coq users already know quite well. However, as I am introducing these concepts, I am also developing my preferred automated proof style, so I think even the chapters on basics are worth reading for experienced Coq hackers. | 166 Some readers have suggested that I give multiple recommended reading orders in this introduction, targeted at people with different levels of Coq expertise. It is certainly true that Part I of the book devotes significant space to basic concepts that most Coq users already know quite well. However, as I am introducing these concepts, I am also developing my preferred automated proof style, so I think even the chapters on basics are worth reading for experienced Coq hackers. |
| 167 | 167 |
| 168 Readers with no prior Coq experience can ignore the preceding discussion! I hope that my heavy reliance on proof automation early on will seem like the most natural way to go, such that you may wonder why others are spending so much time entering sequences of proof steps manually. | 168 Readers with no prior Coq experience can ignore the preceding discussion! I hope that my heavy reliance on proof automation early on will seem like the most natural way to go, such that you may wonder why others are spending so much time entering sequences of proof steps manually. |
| 169 | 169 |
| 170 Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle. When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%. I expect that readers interested in complete understandings will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone. I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets. | 170 Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle. When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%. I expect that readers interested in complete understandings will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone. I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets. |
| 171 | |
| 172 Most chapters end with suggested exercises. Some exercises marked with %``$\star$''%#"star"# are especially difficult or deal with especially advanced subjects that the reader may not wish to master on a first reading. | |
| 171 *) | 173 *) |
| 172 | 174 |
| 173 (** ** On the Tactic Library *) | 175 (** ** On the Tactic Library *) |
| 174 | 176 |
| 175 (** | 177 (** |