Mercurial > cpdt > repo
comparison src/Intro.v @ 39:fd18331e5c0b
Publishing to the web
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 12 Sep 2008 17:18:11 -0400 |
parents | 65314ca099ed |
children | 9bdbc43d510e |
comparison
equal
deleted
inserted
replaced
38:95e24b629ad9 | 39:fd18331e5c0b |
---|---|
165 | 165 |
166 (** | 166 (** |
167 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: |
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># | 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># |
169 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: |
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># | 170 %\begin{center}\url{http://adam.chlipala.net/cpdt/html/toc.html}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/toc.html">http://adam.chlipala.net/cpdt/html/toc.html</a></tt></blockquote># |
171 The source code to the book is also freely available at: | 171 The source code to the book is also freely available at: |
172 %\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># | 172 %\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># |
173 | 173 |
174 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. | 174 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. |
175 | 175 |