Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 45:cb135b19adb8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Propositional logic
author Adam Chlipala <adamc@hcoop.net>
date Sat, 27 Sep 2008 14:57:08 -0400
parents 9bdbc43d510e
children a21447f76aad
comparison
equal deleted inserted replaced
44:b1e137b4aafe 45:cb135b19adb8
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Introducing Inductive Types}% *) 19 (** %\chapter{Introducing Inductive Types}% *)
20 20
21 (** 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. *) 21 (** 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. *)
22 22
23 23
24 (** * Enumerations *) 24 (** * Enumerations *)
25 25
26 (** Coq inductive types generalize the algebraic datatypes found in Haskell and ML. Confusingly enough, inductive types also generalize generalized algebraic datatypes (GADTs), by adding the possibility for type dependency. Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML. 26 (** Coq inductive types generalize the algebraic datatypes found in Haskell and ML. Confusingly enough, inductive types also generalize generalized algebraic datatypes (GADTs), by adding the possibility for type dependency. Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML.