Mercurial > cpdt > repo
diff src/Subset.v @ 451:822442bf6d7f
Proofreading pass through Chapter 5
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 17 Aug 2012 15:39:55 -0400 |
| parents | 2740b8a23cce |
| children | b36876d4611e |
line wrap: on
line diff
--- a/src/Subset.v Fri Aug 17 15:16:08 2012 -0400 +++ b/src/Subset.v Fri Aug 17 15:39:55 2012 -0400 @@ -137,7 +137,7 @@ | S n' -> n' </pre># *) -(** 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. +(** 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. 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]. *)