Mercurial > cpdt > repo

diff src/InductiveTypes.v @ 74:a21447f76aad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Break into Parts
author Adam Chlipala <adamc@hcoop.net>
date Fri, 03 Oct 2008 14:29:21 -0400
parents cb135b19adb8
children a2b14ba218a7
line wrap: on
line diff
--- a/src/InductiveTypes.v	Fri Oct 03 14:14:28 2008 -0400
+++ b/src/InductiveTypes.v	Fri Oct 03 14:29:21 2008 -0400
@@ -16,7 +16,9 @@
 (* end hide *)
 
 
-(** %\chapter{Introducing Inductive Types}% *)
+(** %\part{Basic Programming and Proving}
+
+\chapter{Introducing Inductive Types}% *)
 
 (** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq. *)