Mercurial > cpdt > repo

diff src/InductiveTypes.v @ 43:9bdbc43d510e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make Chap. 3 title less grand
author Adam Chlipala <adamc@hcoop.net>
date Mon, 15 Sep 2008 10:05:37 -0400
parents d45ba7e9b266
children cb135b19adb8
line wrap: on
line diff
--- a/src/InductiveTypes.v	Sat Sep 13 14:35:14 2008 -0400
+++ b/src/InductiveTypes.v	Mon Sep 15 10:05:37 2008 -0400
@@ -16,7 +16,7 @@
 (* end hide *)
 
 
-(** %\chapter{Inductive Types}% *)
+(** %\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 in Coq and shares some "design patterns" for overcoming common pitfalls with them. *)