Mercurial > cpdt > repo
comparison src/Intro.v @ 21:00366a62bd00
Proper title and copyright pages
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 03 Sep 2008 16:37:51 -0400 |
parents | c0cbf324ec7d |
children | 26ad686e68f2 |
comparison
equal
deleted
inserted
replaced
20:c0cbf324ec7d | 21:00366a62bd00 |
---|---|
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |
8 *) | 8 *) |
9 | 9 |
10 (** %\fi | |
11 | |
12 \begin{document} | |
13 | |
14 \maketitle | |
15 | |
16 \thispagestyle{empty} | |
17 \mbox{}\vfill | |
18 \begin{center}% *) | |
19 | |
10 (** | 20 (** |
21 | |
22 Copyright Adam Chlipala 2008. | |
11 | 23 |
12 This work is licensed under a | 24 This work is licensed under a |
13 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 25 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
14 Unported License. | 26 Unported License. |
15 The license text is available at: | 27 The license text is available at: |
16 %\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}% | 28 %\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}% |
17 #<a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">http://creativecommons.org/licenses/by-nc-nd/3.0/</a># | 29 #<a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">http://creativecommons.org/licenses/by-nc-nd/3.0/</a># |
18 | 30 |
19 *) | 31 *) |
32 | |
33 (** %\vfill\mbox{} | |
34 \end{center} | |
35 | |
36 \tableofcontents | |
37 | |
38 \chapter{Introduction}% *) | |
39 | |
40 | |
20 | 41 |
21 | 42 |
22 (** * Whence This Book? *) | 43 (** * Whence This Book? *) |
23 | 44 |
24 (** | 45 (** |
146 This book is generated automatically from Coq source files using the wonderful coqdoc program. The latest PDF version is available at: | 167 This book is generated automatically from Coq source files using the wonderful coqdoc program. The latest PDF version is available at: |
147 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.pdf}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.pdf">http://adam.chlipala.net/cpdt/cpdt.pdf</a></tt></blockquote># | 168 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.pdf}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.pdf">http://adam.chlipala.net/cpdt/cpdt.pdf</a></tt></blockquote># |
148 There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition: | 169 There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition: |
149 %\begin{center}\url{http://adam.chlipala.net/cpdt/html/}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/">http://adam.chlipala.net/cpdt/html/</a></tt></blockquote># | 170 %\begin{center}\url{http://adam.chlipala.net/cpdt/html/}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/">http://adam.chlipala.net/cpdt/html/</a></tt></blockquote># |
150 | 171 |
151 The chapters of this book are named like "Module Foo," rather than having proper names, because literally the entire document is generated by coqdoc, which by default bases chapter structure on the module structure of the development being documented. This chapter is headed "Module Intro" because it comes from a module named [Intro], which comes from a fascinating source file %\texttt{%#<tt>#Intro.v#</tt>#%}% containing nothing but specially-formatted coqdoc comments. | 172 The chapters of this book are named like "Module Foo," rather than having proper names, because literally the entire document is generated by coqdoc, which by default bases chapter structure on the module structure of the development being documented. The next chapter is headed "Module StackMachine" because it comes from a module named [StackMachine], which comes from a source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}%. |
152 | 173 |
153 The source code to the book is also freely available at: | 174 The source code to the book is also freely available at: |
154 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote># | 175 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote># |
155 | 176 |
156 There, you can find all of the code appearing in this book, with prose interspersed in comments, in exactly the order that you find in this document. You can step through the code interactively with your chosen graphical Coq interface. The code also has special comments indicating which parts of the chapters make suitable starting points for interactive class sessions, where the class works together to construct the programs and proofs. The included Makefile has a target %\texttt{%#<tt>#templates#</tt>#%}% for building a fresh set of class template files automatically from the book source. | 177 There, you can find all of the code appearing in this book, with prose interspersed in comments, in exactly the order that you find in this document. You can step through the code interactively with your chosen graphical Coq interface. The code also has special comments indicating which parts of the chapters make suitable starting points for interactive class sessions, where the class works together to construct the programs and proofs. The included Makefile has a target %\texttt{%#<tt>#templates#</tt>#%}% for building a fresh set of class template files automatically from the book source. |