Commit 537bf93d authored by Adam Chlipala's avatar Adam Chlipala

Vertical spacing pass through GeneralRec

parent 296d3c0d
...@@ -220,7 +220,7 @@ End mergeSort. ...@@ -220,7 +220,7 @@ End mergeSort.
Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil). Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
(** [= 1 :: 2 :: 8 :: 19 :: 36 :: 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 *) (* begin thide *)
Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls, Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment