Mercurial > cpdt > repo
comparison src/Large.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 14:23:52 -0400 |
| parents | d7a73ab1df7b |
| children | da576746c3ba |
comparison
equal
deleted
inserted
replaced
| 474:d9e1fb184672 | 475:1fd4109f7b31 |
|---|---|
| 749 (* begin thide *) | 749 (* begin thide *) |
| 750 exact IntProofs.unique_ident. | 750 exact IntProofs.unique_ident. |
| 751 Qed. | 751 Qed. |
| 752 (* end thide *) | 752 (* end thide *) |
| 753 | 753 |
| 754 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. On the other hand, all module values must be determined statically, so modules may not be computed, e.g., within the definitions of normal functions, based on particular function parameters. *) | 754 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many cases. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. On the other hand, all module values must be determined statically, so modules may not be computed, e.g., within the definitions of normal functions, based on particular function parameters. *) |
| 755 | 755 |
| 756 | 756 |
| 757 (** * Build Processes *) | 757 (** * Build Processes *) |
| 758 | 758 |
| 759 (* begin hide *) | 759 (* begin hide *) |