Mercurial > cpdt > repo
comparison src/Large.v @ 437:8077352044b2
A pass over all formatting, after big pile of coqdoc changes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 27 Jul 2012 16:47:28 -0400 |
parents | a54a4a2ea6e4 |
children | 0650420c127b |
comparison
equal
deleted
inserted
replaced
436:5d5e44f905c7 | 437:8077352044b2 |
---|---|
461 | 461 |
462 Undo. | 462 Undo. |
463 info t. | 463 info t. |
464 | 464 |
465 (* begin hide *) | 465 (* begin hide *) |
466 (* begin thide *) | |
466 Definition eir := eq_ind_r. | 467 Definition eir := eq_ind_r. |
468 (* end thide *) | |
467 (* end hide *) | 469 (* end hide *) |
468 | 470 |
469 (** %\vspace{-.15in}%[[ | 471 (** %\vspace{-.15in}%[[ |
470 == simpl in *; intuition; subst; autorewrite with core in *; | 472 == simpl in *; intuition; subst; autorewrite with core in *; |
471 simpl in *; intuition; subst; autorewrite with core in *; | 473 simpl in *; intuition; subst; autorewrite with core in *; |
589 | 591 |
590 Restart. | 592 Restart. |
591 debug eauto 6. | 593 debug eauto 6. |
592 | 594 |
593 (* begin hide *) | 595 (* begin hide *) |
596 (* begin thide *) | |
594 Definition deeeebug := (@eq_refl, @sym_eq). | 597 Definition deeeebug := (@eq_refl, @sym_eq). |
598 (* end thide *) | |
595 (* end hide *) | 599 (* end hide *) |
596 | 600 |
597 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening: | 601 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening: |
598 [[ | 602 [[ |
599 1 depth=6 | 603 1 depth=6 |
753 | 757 |
754 | 758 |
755 (** * Build Processes *) | 759 (** * Build Processes *) |
756 | 760 |
757 (* begin hide *) | 761 (* begin hide *) |
762 (* begin thide *) | |
758 Module Lib. | 763 Module Lib. |
759 Module A. | 764 Module A. |
760 End A. | 765 End A. |
761 Module B. | 766 Module B. |
762 End B. | 767 End B. |
767 Module D. | 772 Module D. |
768 End D. | 773 End D. |
769 Module E. | 774 Module E. |
770 End E. | 775 End E. |
771 End Client. | 776 End Client. |
777 (* end thide *) | |
772 (* end hide *) | 778 (* end hide *) |
773 | 779 |
774 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities. | 780 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities. |
775 | 781 |
776 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work. | 782 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work. |