Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Intro.v Mon Sep 12 11:21:27 2011 -0400 +++ b/src/Intro.v Mon Sep 12 16:42:51 2011 -0400 @@ -168,6 +168,8 @@ 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. 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. + +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. *) (** ** On the Tactic Library *)