Hello,
In my why3 IDE, there is no keyboard shortcut for my installed provers.
Instead of a shortcut, I see « VoidSymbol » for each of my provers.
Is there a way to define a shortcut for a given prover ?
Best,
Sandrine
___
Why3-club mailing list
This looks like a typo in the generated code: (aux: 'xi . 'xi1 -> unit)
should be (aux: 'xi1. 'xi1 -> unit), so possibly a small bug in the code
generator.
On Wed, Nov 14, 2018 at 3:43 PM Benedikt Becker
wrote:
> Hello,
>
> The following program is accepted by the Why3 type checker:
>
> ```
> $
Hello,
The following program is accepted by the Why3 type checker:
```
$ cat test.mlw
let rec f x =
let rec aux y = () in
aux x
```
But the compilation of the extracted OCaml program fails with:
```
$ why3 extract -D ocaml64 test.mlw > test.ml
$ ocamlc -c test.ml
File "test.ml", line 2,
Thanks for your help.
I have removed the « predicate » keyword and it works.
Sandrine
> Le 13 nov. 2018 à 18:25, Andrei Paskevich a écrit :
>
> Hmm, the following works for me in master:
> =
> let predicate lecolor (e1 e2: color) =
> match e1 with
>B -> True
