annotate latex/cpdt.tex @ 492:fa2eb72446a8

Pass through Chapter 2
author Adam Chlipala <adam@chlipala.net>
date Fri, 18 Jan 2013 14:22:50 -0500
parents da576746c3ba
children aed0fcfabdbd
rev   line source
adam@311 1 \documentclass[12pt]{report}
adam@311 2 \usepackage[]{inputenc}
adam@311 3 \usepackage[T1]{fontenc}
adam@468 4 \usepackage{lmodern}
adam@311 5 \usepackage{fullpage}
adam@311 6 \usepackage{coqdoc}
adam@311 7 \usepackage{amsmath,amssymb}
adam@311 8 \usepackage{url}
adam@311 9 \usepackage{makeidx,hyperref}
adam@311 10
adam@479 11 \newcommand{\naive}[0]{na\"ive}
adam@479 12
adam@311 13 \title{Certified Programming with Dependent Types}
adam@311 14 \author{Adam Chlipala}
adam@311 15
adam@311 16 \makeindex
adam@311 17
adam@311 18 \begin{document}
adam@311 19
adam@311 20 \maketitle
adam@311 21
adam@311 22 \thispagestyle{empty}
adam@311 23 \mbox{}\vfill
adam@311 24 \begin{center}
adam@311 25
adam@491 26 Copyright Adam Chlipala 2008-2013.
adam@311 27
adam@311 28
adam@311 29 This work is licensed under a
adam@311 30 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@311 31 Unported License.
adam@311 32 The license text is available at:
adam@311 33
adam@311 34 \end{center}
adam@311 35
adam@311 36 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
adam@311 37
adam@311 38 \phantomsection
adam@311 39 \tableofcontents
adam@311 40
adam@311 41 \include{Intro.v}
adam@311 42 \include{StackMachine.v}
adam@311 43 \include{InductiveTypes.v}
adam@311 44 \include{Predicates.v}
adam@311 45 \include{Coinductive.v}
adam@353 46 \include{Subset.v}
adam@350 47 \include{GeneralRec.v}
adam@311 48 \include{MoreDep.v}
adam@311 49 \include{DataStruct.v}
adam@311 50 \include{Equality.v}
adam@311 51 \include{Generic.v}
adam@311 52 \include{Universes.v}
adam@324 53 \include{LogicProg.v}
adam@311 54 \include{Match.v}
adam@311 55 \include{Reflection.v}
adam@311 56 \include{Large.v}
adam@381 57 \include{ProgLang.v}
adam@383 58 \include{Conclusion.v}
adam@311 59
adam@311 60 \clearpage
adam@311 61 \addcontentsline{toc}{chapter}{Bibliography}
adam@311 62 \bibliographystyle{plain}
adam@311 63 \bibliography{cpdt}
adam@311 64
adam@311 65 \clearpage
adam@311 66 \addcontentsline{toc}{chapter}{Index}
adam@311 67 \printindex
adam@311 68
adam@311 69 \end{document}