Mercurial > cpdt > repo
comparison src/Subset.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 06 Nov 2009 10:52:43 -0500 |
| parents | 939add5a7db9 |
| children | 3227be370687 |
comparison
equal
deleted
inserted
replaced
| 203:71ade09024ac | 204:cbf2f74a5130 |
|---|---|
| 374 (** %\smallskip% | 374 (** %\smallskip% |
| 375 | 375 |
| 376 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." *) | 376 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." *) |
| 377 | 377 |
| 378 (* begin thide *) | 378 (* begin thide *) |
| 379 Notation "x || y" := (if x then Yes else Reduce y) (at level 50). | 379 Notation "x || y" := (if x then Yes else Reduce y). |
| 380 | 380 |
| 381 (** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *) | 381 (** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *) |
| 382 | 382 |
| 383 Section In_dec. | 383 Section In_dec. |
| 384 Variable A : Set. | 384 Variable A : Set. |