diff src/Subset.v @ 74:a21447f76aad

Break into Parts
author Adam Chlipala <adamc@hcoop.net>
date Fri, 03 Oct 2008 14:29:21 -0400
parents 535e1cd17d9a
children ec2c1830a7a1
line wrap: on
line diff
--- a/src/Subset.v	Fri Oct 03 14:14:28 2008 -0400
+++ b/src/Subset.v	Fri Oct 03 14:29:21 2008 -0400
@@ -16,7 +16,9 @@
 (* end hide *)
 
 
-(** %\chapter{Subset Types and Variations}% *)
+(** %\part{Programming with Dependent Types}
+
+\chapter{Subset Types and Variations}% *)
 
 (** So far, we have seen many examples of what we might call "classical program verification."  We write programs, write their specifications, and then prove that the programs satisfy their specifications.  The programs that we have written in Coq have been normal functional programs that we could just as well have written in Haskell or ML.  In this chapter, we start investigating uses of %\textit{%#<i>#dependent types#</i>#%}% to integrate programming, specification, and proving into a single phase. *)
 
@@ -569,10 +571,6 @@
 Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)).
 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)).
 
-Print sumor.
-
-
-
 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
   (right associativity, at level 60).