Mercurial > cpdt > repo

comparison src/Subset.v @ 451:822442bf6d7f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proofreading pass through Chapter 5
author Adam Chlipala <adam@chlipala.net>
date Fri, 17 Aug 2012 15:39:55 -0400
parents 2740b8a23cce
children b36876d4611e
comparison
equal deleted inserted replaced
450:f28bdd8414e0 451:822442bf6d7f
135 let pred_strong1 = function 135 let pred_strong1 = function
136 | O -> assert false (* absurd case *) 136 | O -> assert false (* absurd case *)
137 | S n' -> n' 137 | S n' -> n'
138 </pre># *) 138 </pre># *)
139 139
140 (** The proof argument has disappeared! We get exactly the OCaml code we would have written manually. This is our first demonstration of the main technically interesting feature of Coq program extraction: program components of type [Prop] are erased systematically. 140 (** The proof argument has disappeared! We get exactly the OCaml code we would have written manually. This is our first demonstration of the main technically interesting feature of Coq program extraction: proofs are erased systematically.
141 141
142 We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *) 142 We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *)
143 143
144 (* begin hide *) 144 (* begin hide *)
145 (* begin thide *) 145 (* begin thide *)