Hi Christian, > please find attached the formalization of the merge-sort algorithm as > used in GHC's standard library. See also: > > http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
interesting to read that comment. The exiting quicksort implementation
in HOL is indeed taken from Isabelle's ML library. Don't know what the
ancient motivation for quicksort has been (maybe others can comment on
this).
A critical question: according to the comment, this should easily
generalize to a stable sort_key implementation (as also the current
quicksort does). Have you undertaken this?
All the best,
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
