### changeset 453:e3fa35c750ac

author Adam Chlipala Thu, 23 Aug 2012 16:54:04 -0400 980962258b49 49bd155dfc52 src/GeneralRec.v 1 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/GeneralRec.v	Thu Aug 23 11:06:37 2012 -0400
+++ b/src/GeneralRec.v	Thu Aug 23 16:54:04 2012 -0400
@@ -69,7 +69,7 @@
(** Now, let us try to write the final sorting function, using a natural number "[<=]" test [leb] from the standard library.
[[
Fixpoint mergeSort (ls : list A) : list A :=
-    if leb (length ls) 2
+    if leb (length ls) 1
then ls
else let lss := partition ls in
merge (mergeSort (fst lss)) (mergeSort (snd lss)).
@@ -200,7 +200,7 @@

Hint Resolve partition_wf1 partition_wf2.

-  (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually.  We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type. *)
+  (** To write the function definition itself, we use the %\index{tactics!refine}%[refine] tactic as a convenient way to write a program that needs to manipulate proofs, without writing out those proofs manually.  We also use a replacement [le_lt_dec] for [leb] that has a more interesting dependent type.  (Note that we would not be able to complete the definition without this change, since [refine] will generate subgoals for the [if] branches based only on the _type_ of the test expression, not its _value_.) *)

Definition mergeSort : list A -> list A.
(* begin thide *)
@@ -582,7 +582,7 @@
exists 4; reflexivity.
Qed.

-(** There is another benefit of our new [Fix] compared with one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases.  Consider this simple example, which appeals to another tactic whose definition we elide here. *)
+(** There is another benefit of our new [Fix] compared with the one we used in the previous section: we can now write recursive functions that sometimes fail to terminate, without losing easy reasoning principles for the terminating cases.  Consider this simple example, which appeals to another tactic whose definition we elide here. *)

(* begin hide *)
Ltac looper := unfold leq in *; run;
@@ -759,7 +759,7 @@
(* end thide *)
(* end hide *)

-(** %\vspace{-.15in}%[[
+(** %\vspace{-.3in}%[[
CoFixpoint fib (n : nat) : thunk nat :=
match n with