diff src/Intro.v @ 370:549d604c3d16

Move exercises out of mainline book
author Adam Chlipala <adam@chlipala.net>
date Fri, 02 Mar 2012 09:58:00 -0500
parents 3322367e955d
children f7c2bf7f1324
line wrap: on
line diff
--- a/src/Intro.v	Fri Dec 16 13:28:11 2011 -0500
+++ b/src/Intro.v	Fri Mar 02 09:58:00 2012 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2011, Adam Chlipala
+(* Copyright (c) 2008-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -169,7 +169,7 @@
 
 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.
+Previous versions of the book included some suggested exercises at the ends of chapters.  Since then, I have decided to remove the exercises and focus on the main book exposition.  Especially in the domain of interactive theorem proving, keeping exercises at the proper difficulty level is a lot of work, I have learned!  My advice to readers is to learn to use Coq by getting started applying it in their own real projects, rather than focusing on artificial exercises.
 *)
 
 (** ** On the Tactic Library *)