Mercurial > cpdt > repo
changeset 441:cbfd23b4364d
Vertical spacing pass through GeneralRec
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 01 Aug 2012 15:52:50 -0400 |
| parents | f923024bd284 |
| children | 89c67796754e |
| files | src/GeneralRec.v |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/GeneralRec.v Mon Jul 30 16:50:02 2012 -0400 +++ b/src/GeneralRec.v Wed Aug 01 15:52:50 2012 -0400 @@ -220,7 +220,7 @@ Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil). (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *) -(** Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *) +(** %\smallskip{}%Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *) (* begin thide *) Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,