invalid parenthesis in ocaml extraction
extracting ocaml from the following test.mlw:
use int.Int
let sum (a b : int) = a + b
let apply (f : int -> int -> int) (a b :int) = f a b
let main () = apply sum 1 2
generates:
let sum (a: Z.t) (b: Z.t) : Z.t = infix_pl a b
let apply (f: (Z.t) -> ((Z.t) -> (Z.t))) (a: Z.t) (b: Z.t) : Z.t = (f a) b
let main (_: unit) : Z.t = apply (sum ()) Z.one (Z.of_string "2")
There should not be parenthesis after sum
.
command line:
$ why3 extract -D ocaml64 test.mlw
(version 1.1.1)