Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 469:b36876d4611e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
468:62475ab7570b 469:b36876d4611e
851 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)). 851 comp_eq (Bnd (Bnd m f) g) (Bnd m (fun x => Bnd (f x) g)).
852 red; crush; eauto. 852 red; crush; eauto.
853 Qed. 853 Qed.
854 (* end hide *) 854 (* end hide *)
855 855
856 (** 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. *) 856 (** 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. *)
857 857
858 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)). 858 Notation "x <- m1 ; m2" := (Bnd m1 (fun x => m2)).
859 859
860 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) := 860 CoFixpoint mergeSort'' A (le : A -> A -> bool) (ls : list A) : comp (list A) :=
861 if le_lt_dec 2 (length ls) 861 if le_lt_dec 2 (length ls)