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
___
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 defi
On Fri, 16 Feb 2018, Claude Marché wrote:
>
> 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
