Mercurial > cpdt > repo
comparison src/Subset.v @ 436:5d5e44f905c7
Changes during more coqdoc hacking
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 27 Jul 2012 15:41:06 -0400 |
| parents | 5f25705a10ea |
| children | 8077352044b2 |
comparison
equal
deleted
inserted
replaced
| 435:a54a4a2ea6e4 | 436:5d5e44f905c7 |
|---|---|
| 400 | 400 |
| 401 Notation "'Yes'" := (left _ _). | 401 Notation "'Yes'" := (left _ _). |
| 402 Notation "'No'" := (right _ _). | 402 Notation "'No'" := (right _ _). |
| 403 Notation "'Reduce' x" := (if x then Yes else No) (at level 50). | 403 Notation "'Reduce' x" := (if x then Yes else No) (at level 50). |
| 404 | 404 |
| 405 (** The [Reduce] notation is notable because it demonstrates how [if] is overloaded in Coq. The [if] form actually works when the test expression has any two-constructor inductive type. Moreover, in the [then] and [else] branches, the appropriate constructor arguments are bound. This is important when working with [sumbool]s, when we want to have the proof stored in the test expression available when proving the proof obligations generated in the appropriate branch. | 405 (** The %\coqdocnotation{%#<tt>#Reduce#</tt>#%}% notation is notable because it demonstrates how [if] is overloaded in Coq. The [if] form actually works when the test expression has any two-constructor inductive type. Moreover, in the [then] and [else] branches, the appropriate constructor arguments are bound. This is important when working with [sumbool]s, when we want to have the proof stored in the test expression available when proving the proof obligations generated in the appropriate branch. |
| 406 | 406 |
| 407 Now we can write [eq_nat_dec], which compares two natural numbers, returning either a proof of their equality or a proof of their inequality. *) | 407 Now we can write [eq_nat_dec], which compares two natural numbers, returning either a proof of their equality or a proof of their inequality. *) |
| 408 | 408 |
| 409 Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}. | 409 Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}. |
| 410 refine (fix f (n m : nat) : {n = m} + {n <> m} := | 410 refine (fix f (n m : nat) : {n = m} + {n <> m} := |
| 427 = No | 427 = No |
| 428 : {2 = 3} + {2 <> 3} | 428 : {2 = 3} + {2 <> 3} |
| 429 ]] | 429 ]] |
| 430 *) | 430 *) |
| 431 | 431 |
| 432 (** Note that the [Yes] and [No] notations are hiding proofs establishing the correctness of the outputs. | 432 (** Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs. |
| 433 | 433 |
| 434 Our definition extracts to reasonable OCaml code. *) | 434 Our definition extracts to reasonable OCaml code. *) |
| 435 | 435 |
| 436 Extraction eq_nat_dec. | 436 Extraction eq_nat_dec. |
| 437 | 437 |