Mercurial > cpdt > repo

comparison src/Predicates.v @ 323:3513d8b0531a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thide parsing-motivating definitions at start of Predicates
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Sep 2011 11:08:05 -0400
parents 98e0d957df16
children ad315efc3b6b
comparison
equal deleted inserted replaced
322:98e0d957df16 323:3513d8b0531a
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 16
17 (* Extra definitions to get coqdoc to choose the right fonts. *) 17 (* Extra definitions to get coqdoc to choose the right fonts. *)
18 18
19 (* begin thide *)
19 Inductive unit := tt. 20 Inductive unit := tt.
20 Inductive Empty_set := . 21 Inductive Empty_set := .
21 Inductive bool := true | false. 22 Inductive bool := true | false.
22 Inductive sum := . 23 Inductive sum := .
23 Inductive prod := . 24 Inductive prod := .
24 Inductive and := conj. 25 Inductive and := conj.
25 Inductive or := or_introl | or_intror. 26 Inductive or := or_introl | or_intror.
26 Inductive ex := ex_intro. 27 Inductive ex := ex_intro.
27 Inductive eq := refl_equal. 28 Inductive eq := refl_equal.
28 Reset unit. 29 Reset unit.
30 (* end thide *)
29 (* end hide *) 31 (* end hide *)
30 32
31 (** %\chapter{Inductive Predicates}% *) 33 (** %\chapter{Inductive Predicates}% *)
32 34
33 (** The so-called %\index{Curry-Howard correspondence}``%#"#Curry-Howard correspondence#"#%''~\cite{Curry,Howard}% states a formal connection between functional programs and mathematical proofs. In the last chapter, we snuck in a first introduction to this subject in Coq. Witness the close similarity between the types [unit] and [True] from the standard library: *) 35 (** The so-called %\index{Curry-Howard correspondence}``%#"#Curry-Howard correspondence#"#%''~\cite{Curry,Howard}% states a formal connection between functional programs and mathematical proofs. In the last chapter, we snuck in a first introduction to this subject in Coq. Witness the close similarity between the types [unit] and [True] from the standard library: *)