I suggest to look at http://toccata.lri.fr/gallery/sorting.en.html
and in particular to http://toccata.lri.fr/gallery/mergesort_list.en.html that provides a verified implementation of OCaml's List.sort There is a difference though: since the given 'compare' function should be required to defined a proper order relation, the code is written under a form similar to a functor. This code is not part of Why3's standard library, as far as I know. - Claude Le 16/02/2018 à 11:11, Julia Lawall a écrit : > Hello, > > Does why3 offer sorted lists. Concretely, is it possible to write > something like List.sort compare l in OCaml? I saw the sorted theories in > the List documentation, but I see only lemmas, no functions. Is it > necessary to implement sorting explicitly? > > thanks, > julia > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club