Mercurial > cpdt > repo
comparison src/Subset.v @ 448:2740b8a23cce
Proofreading pass through Chapter 3
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 17 Aug 2012 14:19:59 -0400 |
| parents | 89c67796754e |
| children | 822442bf6d7f |
comparison
equal
deleted
inserted
replaced
| 447:9e3333bd08a1 | 448:2740b8a23cce |
|---|---|
| 457 | 457 |
| 458 Definition eq_nat_dec' (n m : nat) : {n = m} + {n <> m}. | 458 Definition eq_nat_dec' (n m : nat) : {n = m} + {n <> m}. |
| 459 decide equality. | 459 decide equality. |
| 460 Defined. | 460 Defined. |
| 461 | 461 |
| 462 (** Curious readers can verify that the [decide equality] version extracts to the same OCaml code as our more manual version does. That OCaml code had one undesirable property, which is that it uses <<Left>> and <<Right>> constructors instead of the boolean values built into OCaml. We can fix this, by using Coq's facility for mapping Coq inductive types to OCaml variant types.%\index{Vernacular commands!Extract Inductive}% *) | 462 (** Curious readers can verify that the [decide equality] version extracts to the same OCaml code as our more manual version does. That OCaml code had one undesirable property, which is that it uses <<Left>> and <<Right>> constructors instead of the Boolean values built into OCaml. We can fix this, by using Coq's facility for mapping Coq inductive types to OCaml variant types.%\index{Vernacular commands!Extract Inductive}% *) |
| 463 | 463 |
| 464 Extract Inductive sumbool => "bool" ["true" "false"]. | 464 Extract Inductive sumbool => "bool" ["true" "false"]. |
| 465 Extraction eq_nat_dec'. | 465 Extraction eq_nat_dec'. |
| 466 | 466 |
| 467 (** %\begin{verbatim} | 467 (** %\begin{verbatim} |
| 490 | S n1 -> eq_nat_dec' n0 n1) | 490 | S n1 -> eq_nat_dec' n0 n1) |
| 491 </pre># *) | 491 </pre># *) |
| 492 | 492 |
| 493 (** %\smallskip% | 493 (** %\smallskip% |
| 494 | 494 |
| 495 We can build "smart" versions of the usual boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of boolean "or." *) | 495 We can build "smart" versions of the usual Boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of Boolean "or." *) |
| 496 | 496 |
| 497 (* EX: Write a function that decides if an element belongs to a list. *) | 497 (* EX: Write a function that decides if an element belongs to a list. *) |
| 498 | 498 |
| 499 (* begin thide *) | 499 (* begin thide *) |
| 500 Notation "x || y" := (if x then Yes else Reduce y). | 500 Notation "x || y" := (if x then Yes else Reduce y). |