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 |