Mercurial > cpdt > repo
diff src/GeneralRec.v @ 469:b36876d4611e
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 26 Sep 2012 16:35:35 -0400 |
| parents | 4320c1a967c2 |
| children | d9e1fb184672 |
line wrap: on
line diff
--- a/src/GeneralRec.v Wed Sep 05 15:22:13 2012 -0400 +++ b/src/GeneralRec.v Wed Sep 26 16:35:35 2012 -0400 @@ -853,7 +853,7 @@ Qed. (* end hide *) -(** Not only can we define the Fibonacci function with the new monad, but even our running example of merge sort becomes definable. By shadowing our previous notation for "bind,", we can write almost exactly the same code as in our previous [mergeSort'] definition, but with less syntactic clutter. *) +(** Not only can we define the Fibonacci function with the new monad, but even our running example of merge sort becomes definable. By shadowing our previous notation for "bind," we can write almost exactly the same code as in our previous [mergeSort'] definition, but with less syntactic clutter. *) Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).