Thanks for your prompt answer.
Unfortunately, in the instantiation, Why3 complains that "val le = lecolor" is
a syntax error.
Sandrine
> Le 13 nov. 2018 à 14:08, Andrei Paskevich a écrit :
>
> Hi Sandrine,
>
> you try to instantiate a "val predicate" with a purely logical predicate.
> You
Hi Sandrine,
you try to instantiate a "val predicate" with a purely logical predicate.
You should declare "lecolor" as "let predicate" and instantiate using "val
le = lecolor".
Hope it helps,
Andrei
On 13 November 2018 at 14:04, Sandrine Blazy
wrote:
> Hello,
>
> I would like to reuse the
Hello,
I would like to reuse the insertion sort from the Why3 gallery.
The following code was working in version 0.87, but it is not accepted anymore
by version 1.1.0.
What is wrong with my lecolor predicate ?
Best,
Sandrine
module InsertionSort (* from Why3 gallery *)
type elt
val
