Mercurial > cpdt > repo
comparison src/GeneralRec.v @ 441:cbfd23b4364d
Vertical spacing pass through GeneralRec
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 01 Aug 2012 15:52:50 -0400 |
| parents | 8077352044b2 |
| children | e3fa35c750ac |
comparison
equal
deleted
inserted
replaced
| 440:f923024bd284 | 441:cbfd23b4364d |
|---|---|
| 218 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *) | 218 (** The important thing is that it is now easy to evaluate calls to [mergeSort]. *) |
| 219 | 219 |
| 220 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil). | 220 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil). |
| 221 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *) | 221 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *) |
| 222 | 222 |
| 223 (** 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. *) | 223 (** %\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. *) |
| 224 | 224 |
| 225 (* begin thide *) | 225 (* begin thide *) |
| 226 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls, | 226 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls, |
| 227 mergeSort le ls = if le_lt_dec 2 (length ls) | 227 mergeSort le ls = if le_lt_dec 2 (length ls) |
| 228 then let lss := partition ls in | 228 then let lss := partition ls in |