# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223235734 14400
# Node ID d992227e481486c8d1f93c29c4b3b53923200eda
# Parent  15e2b3485dc4d68673e0d6fe3c14303c0096ba91
Start of MoreDep

diff -r 15e2b3485dc4 -r d992227e4814 Makefile
--- a/Makefile	Sun Oct 05 12:12:19 2008 -0400
+++ b/Makefile	Sun Oct 05 15:42:14 2008 -0400
@@ -1,6 +1,6 @@
 MODULES_NODOC := Tactics MoreSpecif
 MODULES_PROSE := Intro
-MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset
+MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset MoreDep
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
diff -r 15e2b3485dc4 -r d992227e4814 src/Intro.v
--- a/src/Intro.v	Sun Oct 05 12:12:19 2008 -0400
+++ b/src/Intro.v	Sun Oct 05 15:42:14 2008 -0400
@@ -193,6 +193,8 @@
 \hline
 Subset Types and Variations & \texttt{Subset.v} \\
 \hline
+More Dependent Types & \texttt{MoreDep.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)
diff -r 15e2b3485dc4 -r d992227e4814 src/MoreDep.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/MoreDep.v	Sun Oct 05 15:42:14 2008 -0400
@@ -0,0 +1,24 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import List.
+
+Require Import Tactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{More Dependent Types}% *)
+
+(** Subset types and their relatives help us integrate verification with programming.  Though they reorganize the certified programmer's workflow, they tend not to have deep effects on proofs.  We write largely the same proofs as we would for classical verification, with some of the structure moved into the programs themselves.  It turns out that, when we use dependent types to their full potential, we warp the development and proving process even more than that, picking up "free theorems" to the extent that often a certified program is hardly more complex than its uncertified counterpart in Haskell or ML.
+
+   In particular, we have only scratched the tip of the iceberg that is Coq's inductive definition mechanism.  The inductive types we have seen so far have their counterparts in the other proof assistants that we surveyed in Chapter 1.  This chapter explores the strange new world of dependent inductive datatypes (that is, dependent inductive types outside [Prop]), a possibility which sets Coq apart from all of the competition not based on type theory. *)
+
diff -r 15e2b3485dc4 -r d992227e4814 src/toc.html
--- a/src/toc.html	Sun Oct 05 12:12:19 2008 -0400
+++ b/src/toc.html	Sun Oct 05 15:42:14 2008 -0400
@@ -10,5 +10,6 @@
 <li><a href="Predicates.html">Inductive Predicates</a>
 <li><a href="Coinductive.html">Infinite Data and Proofs</a>
 <li><a href="Subset.html">Subset Types and Variations</a>
+<li><a href="MoreDep.html">More Dependent Types</a>
 
 </body></html>