Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 74:a21447f76aad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Break into Parts
author Adam Chlipala <adamc@hcoop.net>
date Fri, 03 Oct 2008 14:29:21 -0400
parents cb135b19adb8
children a2b14ba218a7
comparison
equal deleted inserted replaced
73:535e1cd17d9a 74:a21447f76aad
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Introducing Inductive Types}% *) 19 (** %\part{Basic Programming and Proving}
20
21 \chapter{Introducing Inductive Types}% *)
20 22
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. *) 23 (** 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 24
23 25
24 (** * Enumerations *) 26 (** * Enumerations *)