Mercurial > cpdt > repo
diff src/InductiveTypes.v @ 45:cb135b19adb8
Propositional logic
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 27 Sep 2008 14:57:08 -0400 |
| parents | 9bdbc43d510e |
| children | a21447f76aad |
line wrap: on
line diff
--- a/src/InductiveTypes.v Tue Sep 16 16:18:11 2008 -0400 +++ b/src/InductiveTypes.v Sat Sep 27 14:57:08 2008 -0400 @@ -18,7 +18,7 @@ (** %\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. *) +(** 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. *) (** * Enumerations *)